clear a.left.left.
reflexivity.
clear H.clear H1.clear a.right.
- exists.exact e2.exists.exact e1.reflexivity.
+ exists.exact s.exists.exact s1.reflexivity.
clear H.clear a.left.right.
- exists.exact e3.reflexivity.
+ exists.exact s.reflexivity.
qed.
theorem t: 0=0 \to stupidtype.