-
-
-definition r3 : ∀T0:Type.∀T1:T0 → Type.∀T2:∀t0:T0.∀t1:T1 t0.Type.
- ∀T3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
- ∀a0,b0:T0.∀e0:a0 = b0.
- ∀a1:T1 a0.∀b1:T1 b0.∀e1:r1 ?? ?? e0 a1 = b1.
- ∀a2:T2 a0 a1.∀b2:T2 b0 b1.
- ∀e2: r2 ????? e0 ?? e1 a2 = b2.
- T3 a0 a1 a2 → T3 b0 b1 b2.
-intros 12;intro e2;intro H;
-apply (eq_rect' ????? e2);
-apply (R2 ?? ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ? e0 ? e1);
-simplify;assumption;
-qed.
-
-
-apply (R2 ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ??? e0 e1);
-simplify;
-
-
-
-
-
- λT0:Type.λT1:T0 → Type.λT2:∀t0:T0.∀t1:T1 t0.Type.
- λT3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type.
-
- λa0,b0:T0.
- λe0:a0 = b0.
-
- λa1:T1 a0.λb1: T1 b0.
- λe1:r1 ???? e0 a1 = b1.
-
- λa2:T2 a0 a1.λb2: T2 b0 b1.
- λe2:r2 ????? e0 ?? e1 a2 = b2.
-
- λso:T3 a0 a1 a2.
- eq_rect' ?? (λy,p.T3 b0 b1 y)
- (eq_rect' ?? (λy,p.T3 b0 y (r2 ??? ??e0 ??p a2))
- (eq_rect' T0 a0 (λy.λp:a0 = y.T3 y (r1 ?? a0 y p a1) (r2 ??? ??p a2)) so b0 e0)
- ? e1)
- ? e2.
-
-let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝