Proof of Nuprl Lemma : glue-comp

Step * 1 of Lemma glue-comp_wf2

1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : G, phi +⊢ Compositon(T)
7. f : {G, phi ⊢ _:Equiv(T;A)}

8. comp(Glue [phi ⊢→ (T, f)] A)  ∈ composition-function{j:l,i:l}(G;Glue [phi ⊢→ (T;equiv-fun(f))] A)

9. H : CubicalSet{j}
10. K : CubicalSet{j}
11. tau : K j⟶ H
12. sigma : H.𝕀 j⟶ G
13. psi : {H ⊢ _:𝔽}
14. b : {H, psi.𝕀 ⊢ _:(Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma}
15. b0 : {H ⊢ _:((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}
16. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
17. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
18. b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}
19. (phi)sigma ∈ {H.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)}
21. {H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)sigma ⊢ _}
22. H, ((phi)sigma)[0(𝕀)] ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

25. sub_cubical_set{j:l}(H, (∀ (phi)sigma), psi.𝕀; H.𝕀, (psi)p, (phi)sigma)
26. H, (∀ (phi)sigma).𝕀 ⊢ (T)sigma
27. H.𝕀, (phi)sigma +⊢ Compositon((T)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀, (phi)sigma +⊢ Compositon((A)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
29. H.𝕀, (psi)p, (phi)sigma ⊢ (T)sigma
30. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
31. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
32. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
33. unglue(b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

35. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
36. (cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
37. b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]}
38. b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma}
39. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma}
40. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
41. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
⊢ (let a = unglue(b) in
    let a0 = unglue(b0) in
    let a'1 = comp (cA)sigma [psi ⊢→ a] a0 in
    let t'1 = comp (cT)sigma [psi ⊢→ b] b0 in
    let w = pres (equiv-fun(f))sigma [psi ⊢→ b] b0 in
    let st = (t'1 ∨ (b)[1(𝕀)]) in
    let sw = (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) in

    let cF = fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];equiv-fun(((f)sigma)[1(𝕀)]);a'1;

                        (cT)sigma o [1(𝕀)];(cA)sigma o [1(𝕀)]) in
    let z = equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st,  sw)] a'1 in
    let t1 = fiber-member(z) in
    let alpha = fiber-path(z) in

    let a1 = comp (cA)sigma o [1(𝕀)] o p [(((phi)sigma)[1(𝕀)] ∨ psi) ⊢→ ((alpha)p @ q ∨ (a[1])p)] a'1 in

    glue [((phi)sigma)[1(𝕀)] ⊢→ t1] a1)tau
= let a = (unglue(b))tau+ in
   let a0 = (unglue(b0))tau in
   let a'1 = comp (cA)sigma o tau+ [(psi)tau ⊢→ a] a0 in
   let t'1 = comp (cT)sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau in
   let w = pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau in
   let st = (t'1 ∨ ((b)tau+)[1(𝕀)]) in
   let sw = (w ∨ <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p)) in

   let cF = fiber-comp(K, ((phi)sigma o tau+)[1(𝕀)];((T)sigma o tau+)[1(𝕀)];((A)sigma o tau+)[1(𝕀)];

                       equiv-fun(((f)sigma o tau+)[1(𝕀)]);a'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)]) in

   let z = equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (st,  sw)] a'1 in

let t1 = fiber-member(z) in
let alpha = fiber-path(z) in

   let a1 = comp (cA)sigma o tau+ o [1(𝕀)] o p [(((phi)sigma o tau+)[1(𝕀)] ∨ (psi)tau) ⊢→ ((alpha)p @ q ∨ (a[1])p)]

                a'1 in
   glue [((phi)sigma o tau+)[1(𝕀)] ⊢→ t1] a1
∈ {K ⊢ _:(((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[1(𝕀)])tau}
BY
{ ((GenConclTerm ⌜unglue(b)⌝⋅ THENA Auto)
   THEN RenameVar `a' (-2)
   THEN (GenConclTerm ⌜unglue(b0)⌝⋅ THENA Auto)
   THEN RenameVar `a0' (-2)
   THEN (Assert ⌜a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}⌝⋅
   THENM (RepeatFor 2 ((RW (AddrC [2;2] UnfoldTopAbC) 0 THEN Reduce 0))
          THEN RepeatFor 2 ((RW (AddrC [3] UnfoldTopAbC) 0 THEN Reduce 0))

          THEN (((InstLemma `csm-comp_term` [⌜H⌝;⌜psi⌝;⌜(A)sigma⌝;⌜(cA)sigma⌝]⋅ THENA Auto)

THEN (InstHyp [⌜a⌝;⌜a0⌝;⌜K⌝;⌜tau⌝] (-1)⋅
THENA (Try (Trivial)

                              THEN Try ((NthHypSq (-2) THEN Fold `partial-term-0` 0 THEN Trivial))

                              THEN DVar `a'
                              THEN SubsumeTT
                              THEN Auto)
                       )
                 )
                THEN Thin (-2)
                )

          THEN ((InstLemma `comp_term_wf` [⌜H⌝;⌜psi⌝;⌜(A)sigma⌝;⌜(cA)sigma⌝]⋅ THENA Auto)

THEN ((InstHyp [⌜a⌝;⌜a0⌝] (-1)⋅ THENM Fold `partial-term-1` (-1))

                      THENA (Try ((Fold `partial-term-0` 0 THEN Trivial)) THEN DVar `a' THEN SubsumeTT THEN Auto)

                      )
                )
          THEN Thin (-2))
   )) }

1
.....assertion.....
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : G, phi +⊢ Compositon(T)
7. f : {G, phi ⊢ _:Equiv(T;A)}

8. comp(Glue [phi ⊢→ (T, f)] A)  ∈ composition-function{j:l,i:l}(G;Glue [phi ⊢→ (T;equiv-fun(f))] A)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

35. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
36. (cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
37. b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]}
38. b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma}
39. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma}
40. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
41. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. a : {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
44. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
45. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

⊢ a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : G, phi +⊢ Compositon(T)
7. f : {G, phi ⊢ _:Equiv(T;A)}

8. comp(Glue [phi ⊢→ (T, f)] A)  ∈ composition-function{j:l,i:l}(G;Glue [phi ⊢→ (T;equiv-fun(f))] A)

24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}

34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

35. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
36. (cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
37. b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]}
38. b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma}
39. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma}
40. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
41. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
43. a : {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
44. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
45. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

46. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}

47. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}
48. (comp (cA)sigma [psi ⊢→ a] a0)tau
= comp ((cA)sigma)tau+ [(psi)tau ⊢→ (a)tau+] (a0)tau
∈ {K ⊢ _:(((A)sigma)tau+)[1(𝕀)][(psi)tau |⟶ ((a)tau+)[1(𝕀)]]}
49. comp (cA)sigma [psi ⊢→ a] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
⊢ (let a'1 = comp (cA)sigma [psi ⊢→ a] a0 in
    let t'1 = comp (cT)sigma [psi ⊢→ b] b0 in
    let w = pres (equiv-fun(f))sigma [psi ⊢→ b] b0 in
    let st = (t'1 ∨ (b)[1(𝕀)]) in
    let sw = (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) in

    let cF = fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];equiv-fun(((f)sigma)[1(𝕀)]);a'1;

    let a1 = comp (cA)sigma o [1(𝕀)] o p [(((phi)sigma)[1(𝕀)] ∨ psi) ⊢→ ((alpha)p @ q ∨ (a[1])p)] a'1 in

    glue [((phi)sigma)[1(𝕀)] ⊢→ t1] a1)tau
= let a'1 = comp (cA)sigma o tau+ [(psi)tau ⊢→ (a)tau+] (a0)tau in
   let t'1 = comp (cT)sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau in
   let w = pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau in
   let st = (t'1 ∨ ((b)tau+)[1(𝕀)]) in
   let sw = (w ∨ <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p)) in

   let cF = fiber-comp(K, ((phi)sigma o tau+)[1(𝕀)];((T)sigma o tau+)[1(𝕀)];((A)sigma o tau+)[1(𝕀)];

                       equiv-fun(((f)sigma o tau+)[1(𝕀)]);a'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)]) in

   let z = equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (st,  sw)] a'1 in

   let t1 = fiber-member(z) in
   let alpha = fiber-path(z) in
   let a1 = comp (cA)sigma o tau+ o [1(𝕀)] o p [(((phi)sigma o tau+)[1(𝕀)] ∨ (psi)tau) ⊢→

                                                ((alpha)p @ q ∨ ((a)tau+[1])p)] a'1 in

glue [((phi)sigma o tau+)[1(𝕀)] ⊢→ t1] a1
∈ {K ⊢ _:(((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[1(𝕀)])tau}

Latex:

Latex:
1. G : CubicalSet\{j\} 2. A : \{G \mvdash{} \_\} 3. cA : G +\mvdash{} Compositon(A) 4. phi : \{G \mvdash{} \_:\mBbbF{}\} 5. T : \{G, phi \mvdash{} \_\} 6. cT : G, phi +\mvdash{} Compositon(T) 7. f : \{G, phi \mvdash{} \_:Equiv(T;A)\} 8. comp(Glue [phi \mvdash{}\mrightarrow{} (T, f)] A) \mmember{} composition-function\{j:l,i:l\}(G;Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A) 9. H : CubicalSet\{j\} 10. K : CubicalSet\{j\} 11. tau : K j{}\mrightarrow{} H 12. sigma : H.\mBbbI{} j{}\mrightarrow{} G 13. psi : \{H \mvdash{} \_:\mBbbF{}\} 14. b : \{H, psi.\mBbbI{} \mvdash{} \_:(Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma\} 15. b0 : \{H \mvdash{} \_:((Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} (b)[0(\mBbbI{})]]\} 16. G \mvdash{} Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A 17. (Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma = H.\mBbbI{} \mvdash{} Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma 18. b \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\} 19. (phi)sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:\mBbbF{}\} 20. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{}, (phi)sigma \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\} 21. \{H.\mBbbI{}, (phi)sigma \mvdash{} \_\} \msubseteq{}r \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_\} 22. H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} ((T)sigma)[0(\mBbbI{})] 23. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T {}\mrightarrow{} A))sigma)[0(\mBbbI{})]\} 24. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T)sigma)[0(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[0(\mBbbI{})])\} 25. sub\_cubical\_set\{j:l\}(H, (\mforall{} (phi)sigma), psi.\mBbbI{}; H.\mBbbI{}, (psi)p, (phi)sigma) 26. H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} (T)sigma 27. H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((T)sigma) \msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma) 28. H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((A)sigma) \msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma) 29. H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} (T)sigma 30. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 31. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\} 32. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] 33. unglue(b) \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma[(phi)sigma |{}\mrightarrow{} app((equiv-fun(f))sigma; b)]\} 34. unglue(b0) \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][((phi)sigma)[0(\mBbbI{})] |{}\mrightarrow{} app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)]\} 35. (cT)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma) 36. (cA)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma) 37. b0 \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:((T)sigma)[0(\mBbbI{})]\} 38. b \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(T)sigma\} 39. app((equiv-fun(f))sigma; b) \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(A)sigma\} 40. H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} ((T)sigma)[1(\mBbbI{})] 41. \{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\} 42. H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] \mvdash{} (let a = unglue(b) in let a0 = unglue(b0) in let a'1 = comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0 in let t'1 = comp (cT)sigma [psi \mvdash{}\mrightarrow{} b] b0 in let w = pres (equiv-fun(f))sigma [psi \mvdash{}\mrightarrow{} b] b0 in let st = (t'1 \mvee{} (b)[1(\mBbbI{})]) in let sw = (w \mvee{} <>((app((equiv-fun(f))sigma; b)[1])p)) in let cF = fiber-comp(H, ((phi)sigma)[1(\mBbbI{})];((T)sigma)[1(\mBbbI{})];((A)sigma)[1(\mBbbI{})]; equiv-fun(((f)sigma)[1(\mBbbI{})]);a'1;(cT)sigma o [1(\mBbbI{})];(cA)sigma o [1(\mBbbI{})]) in let z = equiv ((f)sigma)[1(\mBbbI{})] [((\mforall{} (phi)sigma) \mvee{} psi) \mvdash{}\mrightarrow{} (st, sw)] a'1 in let t1 = fiber-member(z) in let alpha = fiber-path(z) in let a1 = comp (cA)sigma o [1(\mBbbI{})] o p [(((phi)sigma)[1(\mBbbI{})] \mvee{} psi) \mvdash{}\mrightarrow{} ((alpha)p @ q \mvee{} (a[1])p)] a'1 in glue [((phi)sigma)[1(\mBbbI{})] \mvdash{}\mrightarrow{} t1] a1)tau = let a = (unglue(b))tau+ in let a0 = (unglue(b0))tau in let a'1 = comp (cA)sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} a] a0 in let t'1 = comp (cT)sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau in let w = pres (equiv-fun(f))sigma o tau+ [(psi)tau \mvdash{}\mrightarrow{} (b)tau+] (b0)tau in let st = (t'1 \mvee{} ((b)tau+)[1(\mBbbI{})]) in let sw = (w \mvee{} <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p)) in let cF = fiber-comp(K, ((phi)sigma o tau+)[1(\mBbbI{})];((T)sigma o tau+)[1(\mBbbI{})];((A)sigma o tau+)[1(\mBbbI{})]; equiv-fun(((f)sigma o tau+)[1(\mBbbI{})]);a'1;(cT)sigma o tau+ o [1(\mBbbI{})]; (cA)sigma o tau+ o [1(\mBbbI{})]) in let z = equiv ((f)sigma o tau+)[1(\mBbbI{})] [((\mforall{} (phi)sigma o tau+) \mvee{} (psi)tau) \mvdash{}\mrightarrow{} (st, sw)] a'1 in let t1 = fiber-member(z) in let alpha = fiber-path(z) in let a1 = comp (cA)sigma o tau+ o [1(\mBbbI{})] o p [(((phi)sigma o tau+)[1(\mBbbI{})] \mvee{} (psi)tau) \mvdash{}\mrightarrow{} ((alpha)p @ q \mvee{} (a[1])p)] a'1 in glue [((phi)sigma o tau+)[1(\mBbbI{})] \mvdash{}\mrightarrow{} t1] a1 By Latex: ((GenConclTerm \mkleeneopen{}unglue(b)\mkleeneclose{}\mcdot{} THENA Auto) THEN RenameVar `a' (-2) THEN (GenConclTerm \mkleeneopen{}unglue(b0)\mkleeneclose{}\mcdot{} THENA Auto) THEN RenameVar `a0' (-2) THEN (Assert \mkleeneopen{}a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} a[0]]\}\mkleeneclose{}\mcdot{} THENM (RepeatFor 2 ((RW (AddrC [2;2] UnfoldTopAbC) 0 THEN Reduce 0)) THEN RepeatFor 2 ((RW (AddrC [3] UnfoldTopAbC) 0 THEN Reduce 0)) THEN (((InstLemma `csm-comp\_term` [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}(A)sigma\mkleeneclose{};\mkleeneopen{}(cA)sigma\mkleeneclose{}]\mcdot{} THENA Auto) THEN (InstHyp [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a0\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{}] (-1)\mcdot{} THENA (Try (Trivial) THEN Try ((NthHypSq (-2) THEN Fold `partial-term-0` 0 THEN Trivial)) THEN DVar `a' THEN SubsumeTT THEN Auto) ) ) THEN Thin (-2) ) THEN ((InstLemma `comp\_term\_wf` [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}(A)sigma\mkleeneclose{};\mkleeneopen{}(cA)sigma\mkleeneclose{}]\mcdot{} THENA Auto) THEN ((InstHyp [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a0\mkleeneclose{}] (-1)\mcdot{} THENM Fold `partial-term-1` (-1)) THENA (Try ((Fold `partial-term-0` 0 THEN Trivial)) THEN DVar `a' THEN SubsumeTT THEN Auto) ) ) THEN Thin (-2)) )) Home Index