proposition: Lemma EX_def {_34132 : Type'} : (@EX _34132) = (@ε ((prod nat nat) -> (_34132 -> Prop) -> (list _34132) -> Prop) (fun EX' : (prod nat nat) -> (_34132 -> Prop) -> (list _34132) -> Prop => forall _18143 : prod nat nat, (forall P : _34132 -> Prop, (EX' _18143 P (@nil _34132)) = False) /\ (forall h : _34132, forall P : _34132 -> Prop, forall t : list _34132, (EX' _18143 P (@cons _34132 h t)) = ((P h) \/ (EX' _18143 P t)))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))))).
proof: Proof. exact (eq_refl (@EX _34132)). Qed.
imports: coq theory_hol types