proposition: Lemma INL_def {A B : Type'} : (@inl A B) = (fun a : A => @_mk_sum A B ((fun a' : A => @CONSTR (prod A B) (NUMERAL 0) (@pair A B a' (@ε B (fun v : B => True))) (fun n : nat => @BOTTOM (prod A B))) a)).
proof: Proof. apply fun_ext. intro a. apply _dest_sum_inj. simpl. match goal with [|- ?x = _] => set (r := x) end. unfold _mk_sum. assert (h: exists p, r = _dest_sum p). exists (inl a). simpl. reflexivity. generalize (ε_spec h). set (o := ε (fun p : sum' A B => _dest_sum p = r)). auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance