intro
destruct
reflexivity
left right
constructor 
inversion

simpl
auto
trivial