Step
*
1
of Lemma
csm-case-type
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. a : Base
⊢ A(s I a) ~ let A,F = A
in <λI,a. (A I (s I a)), λI,J,f,a,u. (F I J f (s I a) u)>(a)
BY
{ (RW (SubC (SymbCompC [] 100)) 0 THEN Auto) }
Latex:
Latex:
1. phi : Top
2. A : Top
3. B : Top
4. s : Top
5. I : Base
6. a : Base
\mvdash{} A(s I a) \msim{} let A,F = A
in <\mlambda{}I,a. (A I (s I a)), \mlambda{}I,J,f,a,u. (F I J f (s I a) u)>(a)
By
Latex:
(RW (SubC (SymbCompC [] 100)) 0 THEN Auto)
Home
Index