Intros until 1; XElim H; XEAuto.
Qed.
+ Theorem pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) ->
+ (u:?; f:?) (pr3 c (TTail (Flat f) u t1)
+ (TTail (Flat f) u t2)).
+ Intros; XElim H; XEAuto.
+ Qed.
+
Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) ->
(k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
Intros until 1; XElim H; Intros.
End pr3_props.
Hints Resolve pr3_pr2 pr3_t pr3_pr1
- pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.
+ pr3_thin_dx pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.