-
- Section csub0_pc3. (*****************************************************)
-
- Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
- (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : pr2_pr0 *)
- XAuto.
-(* case 2 : pr2_delta *)
- CSub0Drop; XEAuto.
- Qed.
-
- Theorem csub0_pc2 : (g:?; c1:?; t1,t2:?) (pc2 c1 t1 t2) ->
- (c2:?) (csub0 g c1 c2) -> (pc2 c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : pc2_r *)
- Apply pc2_r; EApply csub0_pr2; XEAuto.
-(* case 2 : pc2_x *)
- Apply pc2_x; EApply csub0_pr2; XEAuto.
- Qed.
-
- Theorem csub0_pc3 : (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
- (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : pc3_r *)
- XAuto.
-(* case 2 : pc3_u *)
- EApply pc3_u; [ EApply csub0_pc2; XEAuto | XAuto ].
- Qed.
-
- End csub0_pc3.
-
- Hints Resolve csub0_pc3 : ltlc.
-
- Section csub0_ty0. (*****************************************************)
-
- Theorem csub0_ty0 : (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
- (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
- (ty0 g c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
- EApply ty0_conv; XEAuto.
-(* case 2 : ty0_sort *)
- XEAuto.
-(* case 3 : ty0_abbr *)
- CSub0Drop; EApply ty0_abbr; XEAuto.
-(* case 4 : ty0_abst *)
- CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
-(* case 5 : ty0_bind *)
- EApply ty0_bind; XEAuto.
-(* case 6 : ty0_appl *)
- EApply ty0_appl; XEAuto.
-(* case 7 : ty0_cast *)
- EApply ty0_cast; XAuto.
- Qed.
-
- Theorem csub0_ty0_ld : (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
- (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
- (ty0 g (CTail c (Bind Abbr) u) t1 t2).
- Intros; EApply csub0_ty0; XEAuto.
- Qed.
-
- End csub0_ty0.
-
- Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
-
- Tactic Definition CSub0Ty0 :=
- Match Context With
- [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
- H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
- LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
- LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].