fact: Axiom thm_MEM_APPEND : forall {_35749 : Type'}, forall x : _35749, forall l1 : list _35749, forall l2 : list _35749, (@List.In _35749 x (@List.app _35749 l1 l2)) = ((@List.In _35749 x l1) \/ (@List.In _35749 x l2)).
imports: coq theory_hol types terms axioms