proposition: Lemma GreatestFixedPoint_ind {fDom : list Type} {fCod : Type} (fDef : funType fDom fCod -> funType fDom fCod) (Inv Post : funType fDom fCod) : refineFun (fDef Inv) Inv -> (refineFun Inv Post) -> refineFun (cl_inf (prefixed_point fDef)) Post.
proof: Proof. intros; rewrite <- H0; simpl in *. destruct (inf_glb (prefixed_point fDef)) as [? ?]. simpl in H1; eapply H1. eapply H. 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