proposition: Lemma fix_dfs : forall m i, ~ is_marked m i -> dfs m i = Dfs dfs m i.
proof: Proof. Proof using. applys~ FixFun2_fix_partial_inv (measure2 (fun m i => nb_unmarked m)) (fun m i m' => nb_unmarked m' < nb_unmarked m). intros m i f1 f2 Hi IH. unfolds Dfs. unfold measure2 in IH. sets_eq N: (nb_unmarked m). let_name_all. let_name_all. let_name_all as aux1. let_name_all as aux2. asserts L: (nb_unmarked m0 < N). subst N m0. applys* add_mark_nb_unmarked. clears m i. gen m0. induction v as [|i v]. simple*. intros m Lt. rew_listx. simpl. asserts [E F]: (aux1 i m = aux2 i m /\ nb_unmarked (aux1 i m) < N). rewrite EQaux1, EQaux2. case_if as C. auto. forwards* [E L]: IH C. split. auto. math. rewrite <- E. applys* IHv. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat