proposition: Lemma corec_ind : forall I A {IA:Inhab A} (E:binary A) (M:family I A) (F:A->A) (Q:I->A->Prop) (x:A), COFE M -> continuous M Q -> E x (F x) -> E = similar M -> (forall i, (forall j, family_r M j i -> Q j x) -> Q i (F x)) -> forall i, Q i x.
proof: Proof. Proof using. introv IA Cofe Conti Eqf SimE Red. subst E. intros i. induction_wf IH: (ofe_wf Cofe) i. apply~ (Conti (rclosure (inverse (family_r M)) i) (fun _ => F x)). intros_all. apply~ equiv_sym. intros j Rji. apply Red. intros k Rkj. apply IH. destruct (rclosure_inv Rji) as [Rji'|Eq]. apply* (trans_inv j). subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)