proposition: Lemma equiv_list_equiv : forall A (E:binary A), equiv E -> equiv (list_equiv E).
proof: Proof. Proof using. introv Equiv. unfold list_equiv. constructor. unfolds. induction x. auto. constructor; dauto. unfolds. induction x; destruct y; introv H; inversions H; dauto. unfolds. induction y; destruct x; destruct z; introv H1 H2; inversions H1; inversions H2; dauto. Qed.
imports: TLC(LibTactics LibLogic LibInt LibList LibRelation LibWf)