---

Step * 1 1 2 of Lemma csm-pi_comp


1. X : Top
2. Y : Top
3. tau : Top
4. A : Top
5. cA : Top
6. cB : Top
7. H : Base
8. sigma : Base
9. phi : Base
10. u : Base
11. a0 : Base
12. I : Base
13. a : Base
14. J : Base
15. f : Base
16. u@0 : Base
⊢ app((a0)p; (revfill(H.((A)tau o sigma)[1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 tau o sigma o p+ o sigma@0 phi u a0);q))[0\000C(𝕀)]) 
~ app((a0)p; (revfill(H.(((A)tau)sigma)[1(𝕀)];λH@0,sigma@0,phi,u,a0. (cA H@0 tau o sigma o p+ o sigma@0 phi u a0);q))[0(\000C𝕀)])
BY
{ (RepUR ``revfill rev_fill_term`` 0 THEN RepeatFor 5 ((EqCD THEN Try (Trivial)))) }

1
1. X : Top
2. Y : Top
3. tau : Top
4. A : Top
5. cA : Top
6. cB : Top
7. H : Base
8. sigma : Base
9. phi : Base
10. u : Base
11. a0 : Base
12. I : Base
13. a : Base
14. J : Base
15. f : Base
16. u@0 : Base
⊢ ((A)tau o sigma)[1(𝕀)] ~ (((A)tau)sigma)[1(𝕀)]

2
1. X : Top
2. Y : Top
3. tau : Top
4. A : Top
5. cA : Top
6. cB : Top
7. H : Base
8. sigma : Base
9. phi : Base
10. u : Base
11. a0 : Base
12. I : Base
13. a : Base
14. J : Base
15. f : Base
16. u@0 : Base
⊢ H.((A)tau o sigma)[1(𝕀)] ~ H.(((A)tau)sigma)[1(𝕀)]

3
1. X : Top
2. Y : Top
3. tau : Top
4. A : Top
5. cA : Top
6. cB : Top
7. H : Base
8. sigma : Base
9. phi : Base
10. u : Base
11. a0 : Base
12. I : Base
13. a : Base
14. J : Base
15. f : Base
16. u@0 : Base
⊢ λH@0,sigma@0,phi,u,a0. (cA H@0 tau o sigma o p+ o sigma@0 phi u a0) ~ λH@0,sigma@0,phi,u,a0. (cA H@0 tau o sigma o p+ \000Co sigma@0 phi u a0)

---

Latex:

---

Latex:

1.  X  :  Top
2.  Y  :  Top
3.  tau  :  Top
4.  A  :  Top
5.  cA  :  Top
6.  cB  :  Top
7.  H  :  Base
8.  sigma  :  Base
9.  phi  :  Base
10.  u  :  Base
11.  a0  :  Base
12.  I  :  Base
13.  a  :  Base
14.  J  :  Base
15.  f  :  Base
16.  u@0  :  Base
\mvdash{}  app((a0)p;  (revfill(H.((A)tau  o  sigma)[1(\mBbbI{})];\mlambda{}H@0,sigma@0,phi,u,a0.  (cA  H@0 
                                                                                                                                              tau  o  sigma  o  p+  o  sigma@0 
                                                                                                                                              phi 
                                                                                                                                              u 
                                                                                                                                              a0);q))[0(\mBbbI{})]) 
\msim{}  app((a0)p;  (revfill(H.(((A)tau)sigma)[1(\mBbbI{})];\mlambda{}H@0,sigma@0,phi,u,a0.  (cA  H@0 
                                                                                                                                            tau  o  sigma  o  p+  o  sigma@0 
                                                                                                                                            phi 
                                                                                                                                            u 
                                                                                                                                            a0);q))[0(\mBbbI{})])


By

---

Latex:
(RepUR  ``revfill  rev\_fill\_term``  0  THEN  RepeatFor  5  ((EqCD  THEN  Try  (Trivial))))

---

Home Index