proposition: Lemma mapii_dep_unfold : forall lf : dep_fun, mapii_dep lf = @F_mapii lf (fun y _ => mapii_dep y).
proof: Proof. intros lf; unfold mapii_dep. refine (Fix_eq _ _ _ _ lf). clear lf; intros [l f] F G H. unfold F_mapii; destruct l as [ | a l]; simpl; auto. rewrite H; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)