Contribution: Cantor

# Library Cantor.prelude.AccP

``` Section restricted_recursion.  Variables (A:Type)(P:A->Prop)(R:A->A->Prop).  Definition restrict (a b:A):Prop :=    P a /\ R a b /\ P b.  Definition well_founded_P := forall (a:A), P a -> Acc restrict a.  Definition P_well_founded_induction_type :        well_founded_P ->        forall X : A -> Type,        (forall x : A, P x -> (forall y : A,P y-> R y x -> X y) -> X x) ->        forall a : A, P a -> X a.   intros W X H a.   pattern a; eapply well_founded_induction_type with (R:=restrict).   unfold well_founded.   split.   unfold well_founded_P in W.   intros; apply W.  case H0.  auto.  intros; apply H.  auto.  intros; apply X0.  unfold restrict; auto.  auto. Defined. End restricted_recursion. Theorem AccElim3 : forall A B C:Type,  forall (RA:A->A->Prop)         (RB:B->B->Prop)         (RC:C->C->Prop),  forall (P : A -> B -> C -> Prop),  (forall x y z,     (forall (t : A), RA t x ->                      forall y' z', Acc RB y' -> Acc RC z' ->                                    P t y' z') ->     (forall (t : B), RB t y ->                      forall z', Acc RC z' -> P x t z') ->     (forall (t : C), RC t z -> P x y t) ->     P x y z) ->   forall x y z, Acc RA x -> Acc RB y -> Acc RC z -> P x y z. Proof.  intros A B C RA RB RC P H x y z Ax; generalize y z; clear y z.  elim Ax; clear Ax x; intros x _ Hrecx y z Ay; generalize z; clear z.  elim Ay; clear Ay y;  intros y _ Hrecy z Az; elim Az; clear Az z; auto. Qed. Theorem accElim3:  forall (A B C:Set)(RA : A -> A ->Prop) (RB : B-> B-> Prop)                    (RC : C -> C -> Prop)(P : A -> B -> C -> Prop),  (forall x y z ,   (forall (t : A), RA t x -> P t y z) ->   (forall (t : B), RB t y -> P x t z) ->   (forall (t : C), RC t z -> P x y t) -> P x y z) ->  forall x y z, Acc RA x -> Acc RB y -> Acc RC z -> P x y z. intros A B C RA RB RC P H x y z Ax Ay Az.  generalize Ax Ay Az.  pattern x, y, z;  eapply AccElim3 with (RA:=RA)(RB:=RB)(RC:=RC) ;eauto.  intros; apply H.  intros;apply H0; auto.  eapply Acc_inv;eauto.  intros;apply H1; auto.  eapply Acc_inv;eauto.  intros;apply H2; auto.   eapply Acc_inv;eauto. Qed. ```