proposition: Theorem tl_app_eq : forall (A : Type)(ls1 ls2 : list A), ls1 <> nil -> tl (ls1 ++ ls2) = (tl ls1) ++ ls2.
proof: Proof. induction ls1; intuition idtac; simpl in *. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation