fact: Axiom thm_FORALL_OPTION_THM : forall {_33228 : Type'}, forall P : (option _33228) -> Prop, (forall x : option _33228, P x) = ((P (@None _33228)) /\ (forall a : _33228, P (@Some _33228 a))).
imports: coq theory_hol types terms axioms