proposition: Lemma axiom_12 : forall {A B : Type'} (r : recspace (prod A B)), ((fun a : recspace (prod A B) => forall sum' : (recspace (prod A B)) -> Prop, (forall a' : recspace (prod A B), ((exists a'' : A, a' = ((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'')) \/ (exists a'' : B, a' = ((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''))) -> sum' a') -> sum' a) r) = ((@_dest_sum A B (@_mk_sum A B r)) = r).
proof: Proof. intros. apply prop_ext. intro h. unfold _mk_sum. rewrite sym. apply (@ε_spec (sum' A B)). apply (h (fun r : recspace (prod A B) => exists x : sum' A B, r = _dest_sum x)). intros. destruct H. destruct H. exists (inl(x)). simpl. exact H. destruct H. exists (inr(x)). simpl. exact H. intro e. rewrite <- e. intros P h. apply h. destruct (_mk_sum r). simpl. left. exists t0. reflexivity. right. exists t0. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance