conj_disj.v

Check and.
Check or.

Check True.
Check False.

Print True.
Print False.

Variable A: Prop.
Variable B: Prop.

Variable a: A.

Definition a_and_b: A -> B -> A /\ B :=
  fun (a: A) (b: B) => conj a b.

Check conj.

Definition a_or_b_continuation_term: forall C: Prop, (A \/ B) -> (A -> C) -> (B -> C) -> C :=
  fun (C: Prop) (disj: A \/ B) (f: A -> C) (g: B -> C) =>
    match disj with
      | or_introl a => f a
      | or_intror b => g b
    end.

Print or_ind.

Definition a_or_b_continuation_induction: forall C: Prop, (A \/ B) -> (A -> C) -> (B -> C) -> C.
Proof.
intros.
induction H.
apply H0.
exact H.
apply H1.
exact H.
Qed.

Print a_or_b_continuation_induction.

Definition a_or_b_continuation_intro_apply: forall C: Prop, (A \/ B) -> (A -> C) -> (B -> C) -> C.
Proof.
intros.
apply or_ind with A B.
exact H0.
exact H1.
exact H.
Qed.

Print a_or_b_continuation_intro_apply.