+ Intros until 1; XElim H; XEAuto.
+ Qed.
+
+ Theorem pr1_tail_1: (u1,u2:?) (pr1 u1 u2) ->
+ (t:?; k:?) (pr1 (TTail k u1 t) (TTail k u2 t)).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Theorem pr1_tail_2: (t1,t2:?) (pr1 t1 t2) ->
+ (u:?; k:?) (pr1 (TTail k u t1) (TTail k u t2)).
+ Intros; XElim H; XEAuto.