- Theorem pc3_gen_not_abst : (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
- (pc3 c (TTail (Bind b) u1 t1)
- (TTail (Bind Abst) u2 t2)
- ) ->
- (pc3 (CTail c (Bind b) u1) t1
- (lift (1) (0) (TTail (Bind Abst) u2 t2))
- )
- .
- Intros b; XElim b; Intros;
- Try EqFalse; Pc3Confluence; Pr3Gen; Pr3Gen;
- Try (Rewrite H1 in H0; Inversion H0);
- Rewrite H1 in H4; Pr3Context;
+ Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
+ (pc3 c (TTail (Bind b) u1 t1)
+ (TTail (Bind Abst) u2 t2)
+ ) ->
+ (pc3 (CTail c (Bind b) u1) t1
+ (lift (1) (0) (TTail (Bind Abst) u2 t2))
+ ).
+ XElim b; Intros;
+ Try EqFalse; Pc3Unfold; Repeat Pr3Gen;
+ Try (Rewrite H0 in H3; TGenBase);
+ Rewrite H1 in H0; Clear H H1 x;