fact: Axiom thm_ALL2_ALL : forall {_36428 : Type'}, forall P : _36428 -> _36428 -> Prop, forall l : list _36428, (@ALL2 _36428 _36428 P l l) = (@List.Forall _36428 (fun x : _36428 => P x x) l).
imports: coq theory_hol types terms axioms