proposition: Lemma equiv_trans: forall L1 L2 L3, Equiv L1 L2 -> Equiv L2 L3 -> Equiv L1 L3.
proof: Proof. unfold Equiv; intros. rewrite H. rewrite H0. intuition. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop