proposition: Lemma induced_eqi {T : Type} (P R : relation T) : PreOrder P -> InducedSym P R -> Equivalence R.
proof: Proof. intros pre ind. split. firstorder. - intros x y Rxy; induced_tac R. - intros x y z Rxy Ryz. destruct pre; induced_tac R. Qed.
imports: Setoid Morphisms Basics