proposition: Lemma INR_def {A B : Type'} : (@inr A B) = (fun a : B => @_mk_sum A B ((fun a' : B => @CONSTR (prod A B) (S (NUMERAL 0)) (@pair A B (@ε A (fun v : A => True)) a') (fun n : nat => @BOTTOM (prod A B))) a)).
proof: Proof. apply fun_ext. intro b. 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 (inr(b)). 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