proposition: Lemma get_put_neq : forall T (t:T) a b u, ~a=b -> get a (put t b u) = get a u.
proof: Proof. intros T t a. induction a. intros. induction u. induction b. induction H; reflexivity. reflexivity. reflexivity. induction b. induction H; reflexivity. reflexivity. reflexivity. intro b. induction b. intros. induction u. simpl. induction a; reflexivity. simpl. reflexivity. intros. induction u. simpl. rewrite IHa. induction a; reflexivity. unfold not; intros. apply H. rewrite H0; reflexivity. simpl. rewrite IHa. reflexivity. unfold not; intros. apply H. rewrite H0; reflexivity. intros. induction u. simpl. induction a; reflexivity. simpl. reflexivity. intro b. induction b. intros. induction u. simpl. induction a; reflexivity. simpl. reflexivity. intros. induction u. simpl. induction a; reflexivity. simpl. reflexivity. intros. induction u. simpl. rewrite IHa. induction a; reflexivity. unfold not; intros. apply H. rewrite H0; reflexivity. simpl. rewrite IHa. reflexivity. unfold not; intros. apply H. rewrite H0; reflexivity. Qed.