proposition: Lemma fix_dep_eq : forall A B (R:binary A) (F:forall x:A, (forall y:A, R y x -> B) -> B) (W:wf R), (forall x f f', (forall y (S:R y x), f y S = f' y S) -> F x f = F x f') -> forall x, fix_dep F W x = F x (fun y _ => fix_dep F W y).
proof: Proof. Proof using. introv Cont. intros. unfold fix_dep. match goal with |- ?g x (W x) = _ => sets G: g end. asserts: (forall x (Ac1 Ac2:Acc R x), G x Ac1 = G x Ac2). clears x. intros x Ac1. induction Ac1 using Acc_inv_dep. intros Ac2. dependent inversion Ac2. simpl. apply~ Cont. case (W x). intros. simpl. apply~ Cont. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)