proposition: Lemma cofe_similar_modulo : forall I A (M:family I A) x y x' y' i, COFE M -> similar M x x' -> similar M y y' -> family_sim M i x' y' -> family_sim M i x y.
proof: Proof. Proof using. intros. apply* (trans_inv x'). apply* (trans_sym_lr y'). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)