Require pr0_lift.
Require pr0_subst1.
Require cpr0_defs.
+Require pc1_props.
Require pc3_props.
Require pc3_gen.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Require ty0_props.
Require ty0_subst0.
Require ty0_gen_context.
Require csub0_defs.
+Require csub0_props.
(*#* #caption "subject reduction" #clauses *)
]; XEAuto
| Idtac ].
Rewrite <- lift_bind; Apply pc3_pc1;
- Apply (pc1_u (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
+ Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
(* case 7: ty0_cast *)
Intros; Inversion H5; Clear H5.
(* case 7.1: pr0_refl *)
(*#* #start file *)
-(*#* #caption "general case" *)
+(*#* #caption "general case without the reduction in the context" *)
(*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->