proposition: Lemma getLast_append_data : forall ls d, snd (getLast (ls ++ d :: nil)) = d.
proof: Proof. induction ls; auto. intros. simpl app. unfold getLast. fold getLast. destruct (ls ++ d :: nil) eqn:Heq. exfalso; eauto. rewrite <- Heq. rewrite IHls. auto. Qed.
imports: Tutorial