- Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->
- (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
- (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
- (pc3 c2 t2 t).
- Intros until 1; XElim H; Intros.
-(* case 1: pc2_r *)
- EApply pc3_pr2_fsubst0; XEAuto.
-(* case 2: pc2_x *)
- Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto.
- Qed.