proposition: Lemma fix_dep_eq_with_proof_irrelevance : 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 x. unfold fix_dep at 1. case (W x). intros K. simpl. apply Cont. intros. pi_rewrite* (K y S). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)