proposition: Lemma set_eq_trans T B (A C : set T) : A <--> B -> B <--> C -> A <--> C.
proof: Proof. by move=> eqAB eqBC; split=> [/eqAB/eqBC|/eqBC/eqAB]. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)