proposition: Lemma rec_eq_ind : forall A B F (P:A->Prop) (R:binary A) (f:A->B) (S:A->B->Prop), (forall x, P x -> f x = F f 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: Proof. Proof using. introv Eqf WfR Red Px. applys~ (>> rec_ind A R Eqf __). intros_all. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)