proposition: Theorem tl_length_pred : forall l: list nat, pred (length l) = length (tl l).
proof: Proof. MProof. destructn 0 asp [ [] ; ["n" ; "l'"] ]. - simpl. reflexivity. - simpl. reflexivity. Qed.
imports: Mtac2.Mtac2 Lists.List