fact: Axiom thm_ALL2_DEF : forall {_34213 _34220 : Type'} (h1' : _34213) (P : _34213 -> _34220 -> Prop) (t1 : list _34213) (l2 : list _34220), ((@ALL2 _34213 _34220 P (@nil _34213) l2) = (l2 = (@nil _34220))) /\ ((@ALL2 _34213 _34220 P (@cons _34213 h1' t1) l2) = (@COND Prop (l2 = (@nil _34220)) False ((P h1' (@hd _34220 l2)) /\ (@ALL2 _34213 _34220 P t1 (@tl _34220 l2))))).
imports: coq theory_hol types terms axioms