; ***********************************************************
; ; Adapt path if necessary:
; (define path "~/minlog/examples/tait/diplomarbeit_schlenker/")

; ; Defines the function "pload" to load files 
; ; from the path defined above
; (define pload (lambda (x) (load (string-append path x))))

; ; Used Modules:
; (pload "./initiate.scm")
; (pload "./defsLamCalc.scm")
; (pload "./defsSubst.scm")
; (pload "./subst_Joachimski_SHORT.scm")
; (pload "./omega.scm")
; (pload "./defsNT.scm")
; (pload "./defsAxiomsSpecial.scm")
; (pload "./trivial.scm")
; (pload "./auxGlobal_SHORT.scm")
; (pload "./defsPred.scm")
; (pload "./proofAxiomsGlobal_SHORT.scm")
;
; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; ============================================
;  Section: The Proofs of the Axioms (Part 1)
; ============================================
; builds upon the proofs in proofAxiomsGlobal;
; contains "Ax1" (the other axioms are covered in Part 2)

; Subsection: "Ax1"
; =================

; Subsubsection: Auxiliaries for "Ax1"
; ::::::::::::::::::::::::::::::::::::
; contains mainly simple facts

; Lemma: "Ax1Aux1"
; ----------------
(add-global-assumption "Ax1Aux1"
 (pf "all n,rs,r,k.
 FoldApp(Var n)rs=r(Var k) ->
 ex rs1. 
 rs = (rs1:+:(Var k):) &
 r = FoldApp (Var n) rs1"))

; Lemma: "Ax1Aux2"
; ----------------
(add-global-assumption "Ax1Aux2"
 (pf "all rs,r,ss.
 BNs (rs:+:r:) ss -> 
 ex ss1,s1. ss = (ss1:+:s1:)"))

; Lemma: "Ax1Aux3"
; ----------------
(add-global-assumption "Ax1Aux3"
 (pf "all rs,r,ss,s.
 BNs (rs:+:r:) (ss:+:s:) ->
 BNs rs ss & BN r s"))

; Lemma: "Ax1Aux4"
; ----------------
(add-global-assumption "Ax1Aux4"
 (pf "all k,s.
 BN (Var k) s -> (Var k) = s"))

; Lemma: "Ax1Aux5"
; ----------------
(add-global-assumption "Ax1Aux5"
 (pf "all n1,n2,rs,ss.
 FoldApp(Var n1)rs=FoldApp(Var n2)ss ->
 (Var n1) = (Var n2) &
 rs = ss"))

; Lemma: "Ax1Aux6"
; ----------------
(add-global-assumption "Ax1Aux6"
 (pf "all rhos4,sigs4,ss3,k,ss4.
 Exps rhos4 sigs4 (ss3:+:(Var k):) ss4 ->
 ex sigs5,sig5,ss5,s5.
 sigs4 = (sigs5 :+: sig5:) &
 ss4 = (ss5 :+: s5:) "))

; Lemma: "Ax1Aux7"
; ----------------
(add-global-assumption "Ax1Aux7"
 (pf "all rhos4,sigs5,sig5,ss3,s3,ss4,s4.
 Exps rhos4 (sigs5:+:sig5:) 
  (ss3:+:s3:) (ss4:+:s4:) ->
 Exps rhos4 sigs5 ss3 ss4 &
 Exp rhos4 sig5 s3 s4"))

; Lemma: "Ax1Aux8"
; ----------------
(add-global-assumption "Ax1Aux8"
 (pf "all rhos4,sig5,k,s5.
 Exp rhos4 sig5(Var k)s5 -> 
 TypJ rhos4 (Var k) sig5"))
; proof by inversion
; (or by the more general ExpTypJ)

; Lemma: "Ax1Aux9"
; ----------------
(add-global-assumption "Ax1Aux9"
 (pf "all rhos,tau,r,k,rho.
 Fr rhos tau r k -> 
 TypJ (rhos:+:ExtCtx rhos k rho) (Var k) rho"))

; Lemma: "Ax1Aux10"
; -----------------
(add-global-assumption "Ax1Aux10"
 (pf "all sigs,rho,sig.
 --->sigs (rho to sig)= 
 --->(sigs :+: rho:) sig"))

; Lemma: "Ax1Aux11"
; -----------------
(add-global-assumption "Ax1Aux11"
 (pf "all rhos,rho,n,rs,k.
 Fr rhos rho (FoldApp (Var n) rs) k ->
 Cor rhos (Var n)"))

; Lemma: "Ax1Aux12"
; -----------------
(add-global-assumption "Ax1Aux12"
 (pf "all rhos,n2,rhos4,k,rho,tau.
 Cor rhos (Var n2) -> 
 rhos4=rhos:+:(ExtCtx rhos k rho) ->
 TypJ rhos4 (Var n2) tau ->
 TypJ rhos (Var n2) tau"))

; Lemma: "Ax1Aux13"
; -----------------
(add-global-assumption "Ax1Aux13"
 (pf "all rhos,sigs5,tau,n2,rs3,k.
 Fr rhos tau (FoldApp(Var n2)rs3) k ->
 TypJ rhos (Var n2)(--->(sigs5) tau) ->
 TypJs rhos rs3 sigs5"))

; Lemma: "BNsTypJ"
; ----------------
(add-global-assumption "BNsTypJ"
 (pf "all rs,ss,rhos,sigs.
 BNs rs ss -> TypJs rhos rs sigs ->
 TypJs rhos ss sigs"))
; proof by BNTypJ

; Lemma: "ExpsRedCtx"
; -------------------
(add-global-assumption "ExpsRedCtx"
 (pf "all rhos,rhos1,sigs,rs,ss.
 Exps (rhos:+:rhos1) sigs rs ss -> 
 TypJs rhos rs sigs ->
 Exps rhos sigs rs ss"))
; clear by definition

; Lemma: "Ax1Aux14"
; -----------------
(add-global-assumption "Ax1Aux14"
 (pf "all r,ss5,s5.
 (FoldApp r ss5) s5 = 
 FoldApp r (ss5:+:s5:)"))

; Lemma: "Ax1Aux15"
; -----------------
(add-global-assumption "Ax1Aux15"
 (pf "all rhos4,rho,k,s5.
 Exp rhos4 rho (Var k) s5 ->
 s5 = Eta rho (Var k)"))
; proof by inversion

; Lemma: "SubThroughEta"
; ----------------------
(add-global-assumption "SubThroughEta"
 (pf "all rho,r,theta.
 Sub (Eta rho r) theta = 
 Eta rho (Sub r theta)"))
; proof by induction on rho

; Lemma: "ABSLift"
; ----------------
; is basically the assertion of
; "Fr rhos r k ->
; ABS k rho r = Abs rho (Lift r 0 1)":

(add-global-assumption "ABSLift"
 (pf "all rhos,rho,r,k.
 Fr rhos rho r k ->
 Sub r (Wrap(Succ(Succ k))
  ((Var map Seq 1 k):+:(Var 0):)) =
 Lift r 0 1"))
; proof by induction on r for the 
; more general lemma:
;
; Fr rhos r k ->
; Sub r (Wrap(Succ(Succ (m+k)))
;  ((Var map Seq 0 m):+:
;  (Var map Seq (m+1) k):+:
;  (Var m):)) =
; Lift r m 1"))

; Lemma: "ExpsTypJs"
; ------------------
(add-global-assumption "ExpsTypJs"
 (pf "all rhos,sigs,rs,ss.
 Exps rhos sigs rs ss ->
 TypJs rhos rs sigs ->
 TypJs rhos ss sigs"))
; proof by ExpTypJ

; Lemma: "Ax1Aux16"
; -----------------
(add-global-assumption "Ax1Aux16"
 (pf "all rhos,n,sigs,tau,ss,k.
 (k < Lh(rhos) -> F) ->
 TypJ rhos (Var n) (---> sigs tau) -> 
 TypJs rhos ss sigs ->
 Fr rhos tau (FoldApp(Var n)ss) k"))

; Lemma: "Ax1Aux17"
; -----------------
(add-global-assumption "Ax1Aux17"
 (pf "all k.
 Sub(Var k)(Wrap(Succ(Succ k))
  ((Var map Seq 1 k):+:(Var 0):)) =
 Var 0"))

; Lemma: "Ax1Aux18"
; -----------------
(add-global-assumption "Ax1Aux18"
 (pf "all k,rho,r,n,rs.
 FoldApp(Var n) rs = ABS k rho r -> F"))

; Lemma: "Ax1Aux19"
; -----------------
(add-global-assumption "Ax1Aux19"
 (pf "all rho3,r3,s3,rs3,r,k.
 FoldApp(Abs rho3 r3)(s3::rs3)=r(Var k) ->
 ex rs4. (s3::rs3) = (rs4:+:(Var k):) &
 r = FoldApp (Abs rho3 r3) rs4"))

; Lemma: "Ax1Aux20"
; -----------------
(add-global-assumption "Ax1Aux20"
 (pf "all rs4,s3,rs3,k.
 rs4=(Nil term) ->
 (s3::rs3)= rs4:+:(Var k): ->
 (Var k) = s3 & 
 rs3 = (Nil term)"))

; Lemma: "Ax1Aux21"
; -----------------
; has non-trivial proof
(add-global-assumption "Ax1Aux21"
 (pf "all r3,k,t2.
 BN(Sub r3(Wrap 0(Var k):))t2 ->
 ex t3. t2 = (Sub t3(Wrap 0(Var k):)) &
 BN r3 t3"))

; Lemma: "Ax1Aux22"
; -----------------
(add-global-assumption "Ax1Aux22"
 (pf "all rhos,rho,sig,r,k.
 Fr rhos (rho to sig) (Abs rho r) k -> 
 Fr (rho::rhos) sig r (Succ k)"))

; Lemma: "Ax1Aux23"
; -----------------
(add-global-assumption "Ax1Aux23"
 (pf "all rhos,tau,r,k,rho.
 Fr rhos tau r (Succ k) ->
 Abs rho r = ABS k rho (Sub r (Wrap 0(Var k):))"))
; proof by induction on k
; Notice: Case k = 0: Trivial
; Case k = n+1: Notice: k is allowed to be in 
; r! But it is lowered during substitution 
; by 1, hence not conflicting with the new k

; Lemma: "Ax1Aux24"
; -----------------
(add-global-assumption "Ax1Aux24"
 (pf "all r,t,k,rhos,rho.
 BN r t -> Fr rhos rho r k ->
 Fr rhos rho t k"))
; proof uses BNTypJ

; Lemma: "Ax1Aux25"
; -----------------
(add-global-assumption "Ax1Aux25"
 (pf "all k,rhos,rho.
 (k < Lh rhos -> F) ->
 TypJ(rhos:+:ExtCtx rhos k rho)(Var k)rho"))

; Lemma: "Ax1Aux26"
; -----------------
(add-global-assumption "Ax1Aux26"
 (pf "all rhos,rho,k.
 (rhos:+:(ExtCtx rhos k rho):+:(Nil type)) =
  rhos:+:(ExtCtx rhos k rho)"))

; Lemma: "Ax1Aux27"
; -----------------
(add-global-assumption "Ax1Aux27"
 (pf "all rhos,rho,sig,r.
 TypJ (rho::rhos) r sig ->
 TypJ rhos (Abs rho r) (rho to sig)"))

; Lemma: "Ax1Aux28"
; -----------------
(add-global-assumption "Ax1Aux28"
 (pf "all rhos,rho,sig,r.
 TypJ rhos (Abs rho r) (rho to sig) ->
 TypJ (rho::rhos) r sig"))

; Lemma: "Ax1Aux29"
; -----------------
(add-global-assumption "Ax1Aux29"
 (pf "all s3,rs3,r5,rs5,k.
 (s3::rs3)=((r5::rs5):+:(Var k):) ->
 s3 = r5 & rs3 =(rs5:+:(Var k):)"))

; Lemma: "Ax1Aux30"
; -----------------
(add-global-assumption "Ax1Aux30"
 (pf "all rho,r,s,ss.
 (FoldApp((Abs rho r) s) ss) =
 (FoldApp(Abs rho r)(s::ss))"))


; Subsubsection: Proof of "Ax1"
; :::::::::::::::::::::::::::::

; Lemma: "Ax1Ind"
; ---------------
(set-goal
 (pf "all rhos,rho,sig,r,k,s.
      Fr rhos(rho to sig)r k ->
      NInd(rhos :+: ExtCtx rhos k rho)sig(r(Var k))s ->
      NInd rhos(rho to sig)r (ABS k rho s)"))

(assume "rhos" "rho" "sig" "r" "k" "s")
(assume "[FrTemp]" "[N]")

; Inversion on N
(inversion "[N]")
(drop "[N]")
(assume "rhos2" "rho2" "r2" "s2" "t2")
(assume 1 2 3 4 5 6 7)

; >>> Simplification
(assert (pf "BN (r(Var k)) t2"))
(simp 8)
(use 4)
(assume "[BN]")
(drop 4)

(assert (pf "
 Exp (rhos:+:ExtCtx rhos k rho) sig t2 s"))
(simp-with 6)
(simp-with 7)
(simp-with 9)
(use 5)
(assume "[ExpTemp]")
(drop 5)

(assert (pf "
 TypJ (rhos:+:ExtCtx rhos k rho) 
 (r(Var k)) sig"))
(simp-with 6)
(simp-with 7)
(simp-with 8)
(use 3)
(assume "[TypJ]")
(drop 3)

(drop  6 7 9)
; <<< End Simplification

; Generalization
(assert (pf "all r. 
 r2 = r (Var k) ->
 Exp(rhos:+:ExtCtx rhos k rho)sig t2 s ->
 Fr rhos(rho to sig)r k ->
 NInd rhos(rho to sig)r(ABS k rho s)"))


; Induction on BN
; %%%%%%%%%%%%%%%
(assert (pf "BN r2 t2"))
(simp "<-" 8)
(use "[BN]")
(elim (pf "BNs rs ss -> T"))
(drop "[BN]")


; Case 1 of BN-Induction
; %%%%%%%%%%%%%%%%%%%%%%
(assume "n2" "rs2" "ss2" "[BNs]" 2)
(drop 14)

(assume "r10")
(assume "[r k]")
(assume "[Exp]")
(assume "[Fr]")

(assert (pf "ex rs1. 
 rs2 = (rs1:+:(Var k):) &
 r10 = FoldApp (Var n2) rs1"))
(use "Ax1Aux1")
(use "[r k]")
(assume "[Ex]")
(by-assume-with "[Ex]" "rs3" "[Inst]")

(assert (pf "ex ss1,s1. ss2 = (ss1:+:s1:)")) 
(use "Ax1Aux2" (pt "rs3") (pt "(Var k)"))
(simp-with "<-" "[Inst]" 'left)
(use "[BNs]")
(assume "[Ex2]")
(by-assume-with "[Ex2]" "ss3" "[Ex2b]")
(by-assume-with "[Ex2b]" "s3" "[Inst2]")

(assert (pf
 "BNs (rs3:+:(Var k):) (ss3:+:s3:)"))
(simp "<-" "[Inst]" 'left)
(simp "<-" "[Inst2]")
(use  "[BNs]")
(assume "[BNs2]")
(drop  "[BNs]")

(assert (pf "BN (Var k) s3"))
(use "Ax1Aux3" (pt "rs3") (pt "ss3"))
(use "[BNs2]")
(assume "[BN k]")

(assert (pf "BNs rs3 ss3"))
(use "Ax1Aux3" (pt "(Var k)") (pt "s3"))
(use "[BNs2]")
(assume "[BNs3]")
(drop "[BNs2]")

(assert (pf "(Var k) = s3"))
(use "Ax1Aux4")
(use "[BN k]")
(assume "[Var k=s3]")

; >>> Simplification
(assert (pf "
 Exp(rhos:+:ExtCtx rhos k rho) sig 
 (FoldApp (Var n2) (ss3:+:(Var k):)) s"))
(simp-with "[Var k=s3]")
(simp-with "<-" "[Inst2]")
(use "[Exp]")
(assume "[Exp2]")
(drop "[Exp]")

(assert (pf "
 Fr rhos(rho to sig) 
  (FoldApp(Var n2)rs3) k"))
(simp-with "<-" "[Inst]" 'right)
(use "[Fr]")
(assume "[Fr2]")
(drop "[Fr]")

(simp-with "[Inst]" 'right)
(drop 14 15 "[Inst]" "[Inst2]"
 "[BN k]" "[Var k=s3]")
; <<< Simplification


; Intro on N
; %%%%%%%%%%
(intro 0 (pt "(FoldApp(Var n2)(ss3))"))

; Case: TypJ
(use "FrDef" (pt "k"))
(use "[Fr2]")

; Case: BN
(intro 0)
(use "[BNs3]")

; Case: Exp

; Inversion on Exp
; %%%%%%%%%%%%%%%%
(inversion "[Exp2]" 
 (pf "Exps rhos sigs rs ss -> T"))
(drop "[Exp2]")


; Case 1 of Exp-Inversion
; %%%%%%%%%%%%%%%%%%%%%%%
(assume "rhos4" "sigs4" "rs4"
 "ss4" "n4" "t4" "rho4")
(assume 1 2 3 4 5 6 7 8)

(assert (pf "(Var n4) = (Var n2) & 
 rs4 = (ss3:+:(Var k):)"))
(use "Ax1Aux5")
(simp 35)
(ng #t)
(prop)
(assume "[Ids]")

; >>> Start Clearance
(drop 32)

(assert (pf "
 s=Eta sig (FoldApp(Var n2)ss4)"))
(simp 34)
(simp 36)
(simp "<-" "[Ids]" 'left)
(use 31)
(assume "[Eta]")
(drop 31 36)

(assert (pf "
 TypJ (rhos:+:ExtCtx rhos k rho)
  (Var n2)(--->sigs4 sig)"))
(simp 33)
(simp 34)
(simp "<-" "[Ids]" 'left)
(use 29)
(assume "[TypJ1]")
(drop 29 35)
(drop 34)

(assert (pf "
 Exps (rhos:+:ExtCtx rhos k rho)
  sigs4 (ss3:+:(Var k):) ss4"))
(simp "<-" "[Ids]" 'right)
(simp 33)
(use 30)
(assume "[Exps]")
(drop 30 33)
; <<< End Clearance

(assert (pf "ex sigs5,sig5,ss5,s5.
 sigs4 = (sigs5 :+: sig5:) &
 ss4 = (ss5 :+: s5:)"))
(use "Ax1Aux6" (pt "(rhos:+:ExtCtx rhos k rho)")
 (pt "ss3") (pt "k"))
(use "[Exps]")
(assume "[Ex3]")
(by-assume-with "[Ex3]" "sigs5" "[Ex3b]")
(by-assume-with "[Ex3b]" "sig5" "[Ex3c]")
(by-assume-with "[Ex3c]" "ss5" "[Ex3d]")
(by-assume-with "[Ex3d]" "s5" "[Inst3]")

; >>> Simplification
(assert (pf "
 Exps (rhos:+:ExtCtx rhos k rho) (sigs5:+:sig5:)
 (ss3:+:(Var k):) (ss5:+:s5:)"))
(simp-with "<-" "[Inst3]" 'left)
(simp-with "<-" "[Inst3]" 'right)
(use "[Exps]")
(assume "[Exps2]")
(drop "[Exps]")
; <<< End Simplification

(assert (pf "Exps (rhos:+:ExtCtx rhos k rho) sigs5 ss3 ss5"))
(use "Ax1Aux7" (pt "sig5") (pt "(Var k)")(pt "s5"))
(use "[Exps2]")
(assume "[Exps3]")

(assert (pf "Exp (rhos:+:ExtCtx rhos k rho) sig5 (Var k) (s5)"))
(use "Ax1Aux7" (pt "sigs5") (pt "ss3")(pt "ss5"))
(use "[Exps2]")
(assume "[Exp3]")

(drop "[Exps2]")

; Part: rho=sig5
(assert (pf "rho=sig5"))

(assert (pf "TypJ (rhos:+:ExtCtx rhos k rho)
 (Var k) sig5"))
(use "Ax1Aux8" (pt "s5"))
(use "[Exp3]")
(assume "[TypJ k 1]")

(assert (pf "TypJ (rhos:+:ExtCtx rhos k rho)
 (Var k) rho"))
(use "Ax1Aux9" (pt "(rho to sig)")
 (pt "(FoldApp(Var n2)rs3)"))
(use "[Fr2]")
(assume "[TypJ k 2]")
(ng)
(simp-with "<-" "[TypJ k 2]" 'right)
(simp-with "<-" "[TypJ k 1]" 'right)
(prop)
(assume "[rho=sig5]")

(assert (pf "TypJ (rhos:+:ExtCtx rhos k rho)
 (Var n2)
 (--->(sigs5) (rho to sig))"))
(simp (pf "rho = sig5"))
(simp (pf "(--->sigs5(sig5 to sig)) =
           (--->(sigs5:+:sig5:) sig)"))
(simp-with "<-" "[Inst3]" 'left)
(simp "<-" (pf "rho = sig5"))
(use "[TypJ1]")
(use "[rho=sig5]")
(use "Ax1Aux10")
(use "[rho=sig5]")
(assume "[TypJ2]")
(drop "[TypJ1]")

; TypJ rhos
(assert (pf "TypJ rhos (Var n2) 
 (--->sigs5(rho to sig))"))

(use "Ax1Aux12" (pt "(rhos:+:ExtCtx rhos k rho)")
 (pt "k") 
 (pt "rho"))
(use "Ax1Aux11" (pt "(rho to sig)") (pt "rs3") 
 (pt "k"))
(use "[Fr2]")
(ng #t)
(prop)
(use "[TypJ2]")
(assume "[TypJ3]")
(drop "[TypJ2]")

; Intermezzo: TypJs ss3
; needed twice
(assert (pf "TypJs rhos ss3 sigs5"))
(use "BNsTypJ" (pt "rs3"))
(use "[BNs3]")
(use "Ax1Aux13" (pt "rho to sig")(pt "n2")
 (pt "k"))
(use "[Fr2]")
(use "[TypJ3]")
(assume "[TypJs ss3]")

; Exps rhos
(assert (pf "Exps rhos sigs5 ss3 ss5"))

(use "ExpsRedCtx" (pt "(ExtCtx rhos k rho)"))
(use "[Exps3]")
(use "[TypJs ss3]")
(assume "[Exps4]")
(drop "[Exps3]")

; Part: Intro Exp
(intro 0 (pt "sigs5") (pt "ss5"))

; TypJ
(use "[TypJ3]")

; Exps
(use "[Exps4]")

; Part: Eta
(assert (pf "
 s = Eta sig ((FoldApp(Var n2)(ss5)) s5)"))
(simp "Ax1Aux14")
(simp-with "<-" "[Inst3]" 'right)
(use "[Eta]")
(assume "[Eta2]")
(drop "[Eta]")

; >>> Simplification
(assert (pf "Exp (rhos:+:ExtCtx rhos k rho)
 rho (Var k) s5"))
(simp-with 
(pf "(rhos:+:(ExtCtx rhos k rho))=
     (rhos:+:(ExtCtx rhos k sig5))"))
(simp-with "[rho=sig5]")
(simp-with 
(pf "(rhos:+:(ExtCtx rhos k sig5))=
     (rhos:+:(ExtCtx rhos k rho))"))
(use "[Exp3]")
(simp-with "[rho=sig5]")
(ng)
(prop)
(simp-with "[rho=sig5]")
(ng)
(prop)
(assume "[Exp4]")
(drop "[Exp3]")
; <<< End: Simplification

(assert (pf "s5 = Eta rho (Var k)"))
(use "Ax1Aux15" (pt "(rhos:+:ExtCtx rhos k rho)"))
(use "[Exp4]")
(assume "[s5=Eta rho(Var k)]")

(assert (pf "
 s = Eta sig ((FoldApp (Var n2) ss5) 
  (Eta rho(Var k)))"))
(simp "<-" "[s5=Eta rho(Var k)]")
(use "[Eta2]")
(assume "[Eta3]")
(drop "[Eta2]")

(simp "[Eta3]")
(ng #t)

(simp (pf "
 Sub (Eta sig(FoldApp(Var n2)ss5 
  (Eta rho(Var k))))
 (Wrap(Succ(Succ k))
  ((Var map Seq 1 k):+:(Var 0):)) =
 Eta sig(Sub (FoldApp(Var n2)ss5 
  (Eta rho(Var k)))
 (Wrap(Succ(Succ k))
  ((Var map Seq 1 k):+:(Var 0):)))"))

(ng #t)

(simp (pf "Sub(FoldApp(Var n2)ss5)
 (Wrap(Succ(Succ k))((Var map Seq 1 k):+:
 (Var 0):)) =
 Lift (FoldApp(Var n2)ss5) 0 1"))

(simp (pf "(Sub(Eta rho(Var k))
 (Wrap(Succ(Succ k))
 ((Var map Seq 1 k):+:(Var 0):))) =
 Eta rho (Sub (Var k)
 (Wrap(Succ(Succ k))
 ((Var map Seq 1 k):+:(Var 0):)))")) 

(simp (pf "(Sub (Var k)
 (Wrap(Succ(Succ k))
 ((Var map Seq 1 k):+:(Var 0):))) =
 (Var 0)"))

(ng #t)
(prop)

(use "Ax1Aux17")
(use "SubThroughEta")
(use "ABSLift" (pt "rhos") 
 (pt "(rho to sig)"))
(use "Ax1Aux16" (pt "sigs5"))
(use "FrDef" (pt "(rho to sig)")
 (pt "(FoldApp(Var n2)rs3)"))
(use "[Fr2]")
(use "[TypJ3]")
(use "ExpsTypJs" (pt "ss3"))
(use "[Exps4]")
(use "[TypJs ss3]")
(use "SubThroughEta")


; Case 2 of Exp-Inversion
; %%%%%%%%%%%%%%%%%%%%%%%
(assume "rhos584" "rhos4" "sigs12" "taus12"
 "rho585" "sig586" "r12" "s587" "k588")
(assume 1 2 3 4 5 6 7 8)

(assert (pf "(FoldApp(Var n2)(ss3:+:(Var k):) = 
 ABS k588 rho585 r12) -> F"))
(use "Ax1Aux18")
(assume "[Contr]")
(prop)

; Case 3 of Exp-Inversion
; %%%%%%%%%%%%%%%%%%%%%%%
(assume "rhos100")
(prop)

; Case 4 of Exp-Inversion
; %%%%%%%%%%%%%%%%%%%%%%%
(assume "rhos5" "sigs5" "r5" 
 "s5" "rs5" "ss5")
(prop)


; Case 2 of BN-Induction
; %%%%%%%%%%%%%%%%%%%%%%
; contradiction of second case:

(assume "rho3" "r3" "s3" "t3" "rs3")
(assume "r4")
(ng)
(prop)


; Case 3 of BN-Induction
; %%%%%%%%%%%%%%%%%%%%%%
(assume "rho3" "r3" "s3" "t" "rs3")
(assume "[BN2]" "[IH BN]")
(drop "[BN]" 8)
(assume "r10")
(assume "[r k]")
(assume "[Exp]")
(assume "[Fr]")

(assert (pf "
 ex rs4. (s3::rs3) = (rs4:+:(Var k):) &
 r10 = FoldApp (Abs rho3 r3) rs4"))
 
(use "Ax1Aux19")
(use "[r k]")
(assume "[Ex]")
(by-assume-with "[Ex]" "rs4" "[Inst]")
(drop "[r k]")

(simp "[Inst]" 'right)


; Case 3.1: "rs4 = (Nil term)"
; %%%%%%%%%%%%%%%%%%%%%%%%%%%%
(cases (pt "rs4"))
(assume "[rs4]")

; >>> Clearance
(assert (pf "(Var k) = s3 &
 rs3 = (Nil term)"))
(use "Ax1Aux20" (pt "rs4")(pt "rs3"))
(use "[rs4]")
(use-with "[Inst]" 'left)
(assume "[Ids]")

(assert (pf "r10=Abs rho3 r3"))
(simp (pf "Abs rho3 r3 = 
 FoldApp (Abs rho3 r3) (Nil term)"))
(simp "<-" "[rs4]")
(use-with "[Inst]" 'right)
(ng)
(prop)
(assume "[r]")
(drop "[Inst]")

(assert (pf "
 BN (Sub r3(Wrap 0 (Var k):)) t"))
(simp (pf "(Sub r3(Wrap 0 (Var k):)) =
 (FoldApp(Sub r3 (Wrap 0 (Var k):)) 
  (Nil term))"))
(simp-with "[Ids]" 'left)
(simp (pf "
 FoldApp(Sub r3(Wrap 0 s3:)) (Nil term) =
 FoldApp(Sub r3(Wrap 0 s3:))rs3"))
(use "[BN2]")
(simp-with "<-" "[Ids]" 'right)
(ng)
(prop)
(ng)
(prop)
(assume "[BN4]")
(drop "[BN2]")
(drop "[rs4]" "[Ids]")

(simp (pf "
 (FoldApp(Abs rho3 r3)(Nil term)) =
 Abs rho3 r3"))
; >>> End Clearance

; rho=rho3
(assert (pf "rho=rho3"))
(assert (pf "TypJ rhos r10 (rho to sig)"))

(use "FrDef" (pt "k"))
(use "[Fr]")
(simp "[r]")
(assume "[temp]")
(ng "[temp]")
(simp-with "<-" "[temp]" 'right 'left) 
(ng)
(prop)
(assume "[rho]")

(assert (pf "r10=Abs rho r3"))
(simp "[rho]")
(use "[r]") 
(assume "[r2]")
(drop "[r]") 

(simp "<-" "[rho]")
(drop "[rho]")

; ex t3
(assert (pf "
 ex t3. t = (Sub t3(Wrap 0(Var k):)) &
 BN r3 t3"))
(use "Ax1Aux21")
(use "[BN4]")
(assume "[Ex2]")
(by-assume-with "[Ex2]" "t3" "[Inst3]")

; Intro N
(intro 0 (pt "Abs rho t3"))
(use "FrDef" (pt "k"))
(simp "<-" "[r2]")
(use "[Fr]")

; BN
(intro 1)
(use-with "[Inst3]" 'right)

;Exp
(assert (pf "Abs rho t3 = 
 ABS k rho (Sub t3 (Wrap 0(Var k):))"))
(use "Ax1Aux23" (pt "(rho::rhos)") (pt "sig"))
(use "Ax1Aux24" (pt "r3"))
(use "[Inst3]" 'right)
(use "Ax1Aux22")
(simp "<-" "[r2]")
(use "[Fr]")
(assume "[ABS]")

(simp "[ABS]")

; Intro Exp:
(simp (pf "rhos = (rhos:+:(Nil type))"))
(intro 1 (pt "ExtCtx rhos k rho")
 (pt "(Nil type)"))

(simp (pf 
 "(rhos:+:(ExtCtx rhos k rho):+:(Nil type)) =
  rhos:+:(ExtCtx rhos k rho)"))

(use "Ax1Aux25")
(use "FrDef" (pt "(rho to sig)") 
 (pt "r10"))
(use "[Fr]")

(use "Ax1Aux26")
(simp "<-" "[Inst3]" 'left)
(use "[Exp]")

(simp "<-" "[ABS]")
(use "Ax1Aux27")
(use "BNTypJ" (pt "r3"))
(use "[Inst3]" 'right)
(use "Ax1Aux28")
(simp "<-" "[r2]")

(use "FrDef" (pt "k"))
(use "[Fr]")
(use "NilAppend")
(ng)
(prop)

; Case 3.1: "rs4 = (r5::rs5)"
; %%%%%%%%%%%%%%%%%%%%%%%%%%%
(assume "r5" "rs5")
(assume "[r4]")

; >>> Start Clearance
(assert (pf "s3 = r5 & 
 rs3 =(rs5:+:(Var k):)"))
(use "Ax1Aux29")
(simp "<-" "[r4]")
(use "[Inst]" 'left)
(assume "[Inst1]")

(assert (pf "
 BN (FoldApp(Sub r3(Wrap 0 r5:))
  (rs5:+:(Var k):)) t"))
(simp "<-" "[Inst1]" 'left)
(simp "<-" "[Inst1]" 'right)
(use "[BN2]")
(assume "[BN3]")
(drop "[BN2]")

(assert (pf "
 r10=FoldApp(Abs rho3 r3)(r5::rs5)"))
(simp "<-" "[r4]" 'right)
(use "[Inst]")
(assume "[Inst2]")
(drop "[Inst]" "[r4]")
; >>> End Clearance

(assert (pf "
 NInd rhos(rho to sig) 
  (FoldApp(Sub r3(Wrap 0 r5:))rs5)
  (ABS k rho s)"))

(use "[IH BN]")

; Fold
(simp "[Inst1]" 'left)
(simp "[Inst1]" 'right)
(simp "Ax1Aux14")
(ng)
(prop)

; Exp
(use "[Exp]")

; Fr
(assert (pf "Fr rhos(rho to sig) 
 (FoldApp ((Abs rho3 r3)r5) rs5) k"))
(simp "Ax1Aux30")
(simp "<-" "[Inst2]")
(use "[Fr]")
(assume "[Fr1]")

(use "FrDefRev")
(use "TypJFoldHead" 
 (pt "(Abs rho3 r3 r5)"))
(use "FrDef" (pt "k"))
(use "[Fr1]")
(use "SR" (pt "rho3"))
(use "CorTypJ")
(use "TypJFoldHeadCor" (pt "(rho to sig)")
 (pt "rs5"))
(use "FrDef" (pt "k"))
(use "[Fr1]")
(use "FrDef" (pt "(rho to sig)")
 (pt "(FoldApp(Abs rho3 r3 r5)rs5)"))
(use "[Fr1]")

(assume "[N2]")

(inversion "[N2]")
(assume "rhos4" "rho4" "r4" "s4" "t4")
(assume 1 2 3 4 5 6 7)

; >>> Start Clearance
(assert (pf "
 BN (FoldApp(Sub r3(Wrap 0 r5:))rs5) t4"))
(simp 30)
(use 26)
(assume "[BN4]")
(drop 26 "[BN3]")

(assert (pf "
 Exp rhos (rho to sig) t4 (ABS k rho s)"))
(simp 28)
(simp 29)
(simp 31)
(use 27)
(assume "[Exp2]")

(drop 27 28 29 30 31 "[Exp]")
; <<< End Clearance

(intro 0 (pt "t4"))

; TypJ
(simp "<-" "[Inst2]")
(use "FrDef" (pt "k"))
(use "[Fr]")

; BN
(simp (pf "FoldApp(Abs rho3 r3)(r5::rs5) =
 FoldApp((Abs rho3 r3)r5) rs5"))

(intro 2)
(use "[BN4]")
(ng)
(prop)
(use "[Exp2]")

; Final Parts (trivial)
; =====================
(prop)

(assume "r3" "s3" "rs3" "ss3")
(prop)

(assume "[Gen]")
(use "[Gen]")
(simp 8)
(ng)
(prop)
(use "[ExpTemp]")
(use "[FrTemp]")
(save "Ax1Ind")

; Lemma: "Ax1"
; -----------
(set-goal
 (pf "all rhos,rho,sig,r,k,s.
      Fr rhos(rho to sig)r k ->
      N (rhos :+: ExtCtx rhos k rho) sig (r(Var k)) s ->
      N rhos (rho to sig) r (ABS k rho s)"))

(assume "rhos" "rho" "sig" "r" "k" "s")
(assume 1 2)
(use "NDefRev")
(assert (pf "NInd (rhos:+:ExtCtx rhos k rho)
 sig(r(Var k))s"))
(use "NDef")
(use 2)
(assert (pf "Fr rhos(rho to sig)r k"))
(use 1)

(use "Ax1Ind")
(save "Ax1")