proposition: Lemma standard_gnaw_plus : forall (t1 t2 i:nat)(alpha : T1) , standard_gnaw i alpha (t1 + t2)%nat = standard_gnaw (t1 +i)%nat (standard_gnaw i alpha t1) t2.
proof: Proof. induction t1; simpl. - trivial. - intros t2 i alpha; rewrite IHt1. replace (t1 + S i)%nat with (S (t1 + i))%nat; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)