proposition: Lemma get_put_eq1 : forall T (t:T) a u, get a (put t a u) = t.
proof: Proof. intros. generalize a. induction u. intros. induction a0; try reflexivity. simpl. assumption. simpl. assumption. intros. induction a0; try reflexivity. simpl. auto. simpl; auto. Qed.