proposition: Lemma FixFun3_fix_partial : forall A1 A2 A3 (R:binary (A1*A2*A3)) (P:A1->A2->A3->Prop) B {IB:Inhab B} F (f:A1->A2->A3->B), f = FixFun3 F -> wf R -> (forall x1 x2 x3 f1 f2, P x1 x2 x3 -> (forall y1 y2 y3, P y1 y2 y3 -> R (y1,y2,y3) (x1,x2,x3) -> f1 y1 y2 y3 = f2 y1 y2 y3) -> F f1 x1 x2 x3 = F f2 x1 x2 x3) -> (forall x1 x2 x3, P x1 x2 x3 -> f x1 x2 x3 = F f x1 x2 x3).
proof: Proof. Admitted. Arguments FixFun3_fix_partial [A1] [A2] [A3] R P [B] {IB} [F] [f]. Lemma FixFun4_fix_partial : forall A1 A2 A3 A4 (R:binary (A1*A2*A3*A4)) (P:A1->A2->A3->A4->Prop) B {IB:Inhab B} F (f:A1->A2->A3->A4->B), f = FixFun4 F -> wf R -> (forall x1 x2 x3 x4 f1 f2, P x1 x2 x3 x4 -> (forall y1 y2 y3 y4, P y1 y2 y3 y4 -> R (y1,y2,y3,y4) (x1,x2,x3,x4) -> f1 y1 y2 y3 y4 = f2 y1 y2 y3 y4) -> F f1 x1 x2 x3 x4 = F f2 x1 x2 x3 x4) -> (forall x1 x2 x3 x4, P x1 x2 x3 x4 -> f x1 x2 x3 x4 = F f x1 x2 x3 x4). Admitted. Arguments FixFun4_fix_partial [A1] [A2] [A3] [A4] R P [B] {IB} [F] [f]. Lemma FixFun5_fix_partial : forall A1 A2 A3 A4 A5 (R:binary (A1*A2*A3*A4*A5)) (P:A1->A2->A3->A4->A5->Prop) B {IB:Inhab B} F (f:A1->A2->A3->A4->A5->B), f = FixFun5 F -> wf R -> (forall x1 x2 x3 x4 x5 f1 f2, P x1 x2 x3 x4 x5 -> (forall y1 y2 y3 y4 y5, P y1 y2 y3 y4 y5 -> R (y1,y2,y3,y4,y5) (x1,x2,x3,x4,x5) -> f1 y1 y2 y3 y4 y5 = f2 y1 y2 y3 y4 y5) -> F f1 x1 x2 x3 x4 x5 = F f2 x1 x2 x3 x4 x5) -> (forall x1 x2 x3 x4 x5, P x1 x2 x3 x4 x5 -> f x1 x2 x3 x4 x5 = F f x1 x2 x3 x4 x5). Admitted. Arguments FixFun5_fix_partial [A1] [A2] [A3] [A4] [A5] R P [B] {IB} [F] [f]. Lemma rec_ind : forall A B F (E:binary B) (P:A->Prop) (R:binary A) (f:A->B) (S:A->B->Prop), (forall x, P x -> E (f x) (F f x)) -> (forall x, pred_compatible E (S x)) -> wf R -> (forall x f', P x -> (forall y, P y -> R y x -> S y (f' y)) -> S x (F f' x)) -> forall x, P x -> S x (f x). Proof using. introv Eqf Comp WfR Red. intros x. induction_wf IH: WfR x. intros Px. eapply Comp. apply~ Red. apply~ Eqf. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)