fact: Axiom thm_ASSOC : forall {_34421 _34427 : Type'} (h : prod _34427 _34421) (a : _34427) (t : list (prod _34427 _34421)), (@ASSOC _34421 _34427 a (@cons (prod _34427 _34421) h t)) = (@COND _34421 ((@fst _34427 _34421 h) = a) (@snd _34427 _34421 h) (@ASSOC _34421 _34427 a t)).
imports: coq theory_hol types terms axioms