proposition: Lemma corec_rec_similar : forall I A B (M:family I B) (P:A->Prop) (R:binary A), similar (corec_rec_family M P R) = (fun f1 f2 => forall x, P x -> similar M (f1 x) (f2 x)).
proof: Proof. Proof using. extens. intros f1 f2. unfold similar. simpl. iff H. intros. apply~ (H (i,x)). intros [i x]. intros. apply~ H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)