∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
#A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
#A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
qed.
lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
∀l1,l2. all2 … P l1 l2 → all2 … P (tail … l1) (tail … l2).
#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
qed.
lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
∀l1,l2. all2 … P l1 l2 → all2 … P (tail … l1) (tail … l2).
#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]