proposition: Lemma MEM_def {_25376 : Type'} : (@In _25376) = (@ε ((prod nat (prod nat nat)) -> _25376 -> (list _25376) -> Prop) (fun MEM' : (prod nat (prod nat nat)) -> _25376 -> (list _25376) -> Prop => forall _17995 : prod nat (prod nat nat), (forall x : _25376, (MEM' _17995 x (@nil _25376)) = False) /\ (forall h : _25376, forall x : _25376, forall t : list _25376, (MEM' _17995 x (@cons _25376 h t)) = ((x = h) \/ (MEM' _17995 x t)))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))))))).
proof: Proof. generalize (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0))))))), NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))))); intro p. apply fun_ext; intro x. apply fun_ext; intro l. match goal with |- _ = ε ?x _ _ _=> set (Q := x) end. assert (i : exists q, Q q). exists (fun _=> @In _25376). unfold Q. intro. simpl. split. trivial. intros. apply prop_ext. intro. destruct H. symmetry in H. left. exact H. right. exact H. intro. destruct H. left. symmetry in H. exact H. right. exact H. generalize (ε_spec i). intro H. symmetry. induction l; simpl. apply H. rewrite <- IHl. transitivity ((x = a \/ ε Q p x l)). apply H. apply prop_ext. intro. destruct H0. left. symmetry. exact H0. right. exact H0. intro. destruct H0. left. symmetry. exact H0. right. exact H0. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List