qed.
lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
∀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_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
∀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 ]