proposition: Lemma Finish_refining_LeastFixedPoint {fDom : list Type} {recT fCod : Type} {P : recT -> recT -> Prop} (wf_P : well_founded P) (fDef : funType (recT :: fDom) fCod -> funType (recT :: fDom) fCod) (fDef_monotone : forall rec rec', refineFun rec rec' -> refineFun (fDef rec) (fDef rec')) (fDef' : forall r, (forall r', P r' r -> cfunType fDom fCod) -> cfunType fDom fCod) : (forall r, respectful_hetero (funType (recT :: fDom) fCod) (forall r', P r' r -> cfunType fDom fCod) (fun _ => funType fDom fCod) (fun _ => cfunType fDom fCod) (fun f f' => forall r' wf_r, @refineFun fDom fCod (f r') ((Lift_cfunType _ _ (f' r' wf_r)))) (fun rec rec' f f' => @refineFun fDom fCod f (Lift_cfunType _ _ f')) (fun rec => fDef rec r) (fDef' r)) -> refineFun (LeastFixedPoint fDef ) (Lift_cfunType (recT :: fDom) fCod (Fix wf_P _ fDef' )).
proof: Proof. unfold LeastFixedPoint, respectful_hetero; intros. simpl in H. simpl. simpl in H. intros; pattern t; eapply (well_founded_ind wf_P). simpl; intros; rewrite Fix_eq. pose proof (proj1 (Is_GreatestFixedPoint (O := @funDefOps (recT :: fDom) fCod) _ (fDef_monotone))); etransitivity. eapply H1; eauto. eapply H; eauto. intros; f_equal. repeat (eapply functional_extensionality_dep; intros); eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Sets.Ensembles Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation Fiat.Computation.SetoidMorphisms Coq.Logic.FunctionalExtensionality