proposition: Theorem cover_one_inv : forall t1 t2, cover (t1 :: []) t2 -> t1 = t2.
proof: Proof. intros t1 t2 H; inversion H; auto. absurd (length (t1 :: []) = length (t0 :: t3 :: l2)). simpl in |- *; intros; discriminate. apply Permutation_length with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)