-theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
- \forall p2,r2. (p2 + q == r2) \to
- \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
- intros 4. elim H; clear H q r1;
- [ lapply linear nplus_gen_zero_2 to H1. subst
- | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
- lapply linear nplus_gen_succ_2 to H4. decompose. subst
- ]; auto.
+theorem nplus_comm_1: ∀p1, q, r1. p1 ⊕ q ≍ r1 → ∀p2, r2. p2 ⊕ q ≍ r2 →
+ ∀x. p2 ⊕ r1 ≍ x → ∀y. p1 ⊕ r2 ≍ y → x = y.
+ intros 4; elim H; clear H q r1;
+ [ lapply linear nplus_inv_zero_2 to H1
+ | lapply linear nplus_inv_succ_2 to H3.
+ lapply linear nplus_inv_succ_2 to H4. decompose. destruct.
+ lapply linear nplus_inv_succ_2 to H5. decompose
+ ]; destruct; autobatch.
+qed.
+
+theorem nplus_comm_1_rew: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ q ≍ r2 →
+ ∀s. p1 ⊕ r2 ≍ s → p2 ⊕ r1 ≍ s.
+ intros 4; elim H; clear H q r1;
+ [ lapply linear nplus_inv_zero_2 to H1. destruct
+ | lapply linear nplus_inv_succ_2 to H3. decompose. destruct.
+ lapply linear nplus_inv_succ_2 to H4. decompose. destruct
+ ]; autobatch.