-| rewrite > true_to_sigma_p_Sn
- [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
- [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
- [ rewrite > assoc_plus in \vdash (? ? ? %).
- rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
- rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
- rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
- rewrite < assoc_plus in \vdash (? ? ? %).
- apply eq_f.
- assumption
- | reflexivity
- ]
- | reflexivity
- ]
- | reflexivity
- ]
-]
+| apply (bool_elim ? (p n1)); intro;
+ [ rewrite > true_to_sigma_p_Sn
+ [ rewrite > (true_to_sigma_p_Sn n1 p f)
+ [ rewrite > (true_to_sigma_p_Sn n1 p g)
+ [ rewrite > assoc_plus in \vdash (? ? ? %).
+ rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
+ rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
+ rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
+ rewrite < assoc_plus in \vdash (? ? ? %).
+ apply eq_f.
+ assumption]]]
+ assumption
+ | rewrite > false_to_sigma_p_Sn
+ [ rewrite > (false_to_sigma_p_Sn n1 p f)
+ [ rewrite > (false_to_sigma_p_Sn n1 p g)
+ [assumption]]]
+ assumption
+]]