
Require Refine.

Inductive term : Set :=
	a : term
      | f : term -> term
      | cons : term -> term -> term
.

Inductive p : term -> Prop :=
    p_a : (p a)
  | p_f : (x:term) (p x) -> (p (f x))
with q : term -> Prop :=
    q_a : (q a)
  | q_f : (x:term) (q x) -> (q (f x)).

Remark rem_pqa : ((x:term) (p x) -> (q x)) -> (p a) -> (q a).
Proof.
  Intros. Apply q_a; Assumption.
Defined.

Remark rem_2 : ((x:term) (p x) -> (q x)) -> (_x1:term) (p _x1) -> (q _x1).
Proof.
  Intros Hrec. Intros _x1. Cut (p _x1)->(q _x1). Tauto.
  Exact (Hrec _x1).
Defined.

Remark rem_3 : ((x:term) (p x) -> (q x)) -> (_x1:term) (p _x1) -> (q _x1) \/ False.
Proof.
  Intros Hrec. Intros _x1. Intros H1. Cut (q _x1). Tauto.
  Apply (rem_2 Hrec _x1); Assumption.
Defined.

Remark rem_4 : ((x:term) (p x) -> (q x)) -> (_x1:term) (p _x1) -> (q (f _x1)).
Proof.
  Intros Hrec. Intros _x1. Intros H1. Case (rem_3 Hrec _x1 H1).
  Clear Hrec H1. Intros. Apply q_f; Tauto.
  Clear Hrec H1. Tauto.
Defined.

Inductive or_1 [H1:Prop] : Prop :=
    or_1_intro_1 : H1 -> (or_1 H1).

Remark rem_5 : (_x1:term) (p (f _x1)) -> (or_1
    (p _x1)
).
Proof.
  Intros. Inversion H.
  Intros. Apply or_1_intro_1; Tauto.
Qed.

Remark rem_pqf : ((x:term) (p x) -> (q x)) -> (_x1:term) (p (f _x1)) -> (q (f _x1)).
Proof.
  Intros Hrec. Intros _x1. Intros H. Elim (rem_5 _x1 H); Intros.
  Apply (rem_4 Hrec _x1); Tauto.
Defined.

(*
Proof.
  Intros Hrec. Intros _x1. Cut (p (f _x1))->(q (f _x1)). Tauto.
  Exact (Hrec (f _x1)).
Defined.
*)

Inductive ex_0 [A: Set; P : Prop] : Prop :=
    ex_0_intro : P -> (ex_0 A P).

Inductive ex_1 [A: Set; P :  A -> Prop] : Prop :=
    ex_1_intro : (x1:A)(P x1) -> (ex_1 A P).

Inductive or_2 [H1,H2:Prop] : Prop :=
    or_2_intro_1 : H1 -> (or_2 H1 H2)
  | or_2_intro_2 : H2 -> (or_2 H1 H2).

Remark rem_6 : (x:term) (p x) -> (or_2
  (ex_0 term x=a)
  (ex_1 term [_x:term] x=(f _x))
  ).
Proof.
  Intros. Inversion H.
  Apply or_2_intro_1. EApply (ex_0_intro term). Reflexivity.
  Apply or_2_intro_2. EApply (ex_1_intro term). Reflexivity.
Defined.

Remark rem_induct : (x:term) (p x) -> (q x).
Proof.
  Fix epsilon_mp_pq 1. Intro x.
  Case x; First [Exact (rem_pqa epsilon_mp_pq)
	       | Intro _x; Exact (rem_pqf epsilon_mp_pq _x)
	       | Intros until 1; Inversion H].
Defined.

(*
Intros.
  Apply rem_pqa; Assumption.
  Apply rem_pqf; Assumption.
Defined.
*)

(*
Proof.
  Fix epsilon_mp_pq 2.
  Intro x. Intros H_p. Generalize H_p. Elim (rem_6 x H_p); Intro H; Case H; Clear H H_p.
  Intros H. Rewrite H. Intros. Apply rem_pqa; Assumption.
  Intros _x1 H. Rewrite H. Intros. Apply rem_pqf; Assumption.
Defined.
*)

(*
Variable epsilon_mp_pq : (x:term) (p x) -> (q x).
Transparent sym_eq.
Eval Compute in [x:term; H_p:(p x)]
  (or_2_ind (ex_0 term x=a) (ex_1 term [_x:term]x=(f _x)) (p x)->(q x)
    [H:(ex_0 term x=a)]
     Cases H of
       (ex_0_intro H0) => 
        (eq_ind_r term a [t:term](p t)->(q t)
          [H_p0:(p a)](rem_pqa epsilon_mp_pq H_p0) x H0)
     end
    [H:(ex_1 term [_x:term]x=(f _x))]
     Cases H of
       (ex_1_intro _x1 H0) => 
        (eq_ind_r term (f _x1) [t:term](p t)->(q t)
          [H_p0:(p (f _x1))](rem_pqf epsilon_mp_pq _x1 H_p0) x H0)
     end (rem_6 x H_p) H_p).
*)

