proposition: Lemma atom_single_atom a i b: tatom _ a ⋅ ttsingle i ⋅ tatom _ b ≡ tsingle' a i b.
proof: Proof. intro x. split. - intros [uv [u <- [v Hv Huvw]] [w <- Huvw']]. destruct v as [|c j [d|]]; try elim Hv. destruct Hv. inversion Huvw. simpl. subst. setoid_rewrite <- (tapp_tail_head Huvw'). now apply tapp_x_nil_eq in Huvw' as [-> ->]. - intros <-. exists (tcons a i (tnil b)). eexists. reflexivity. exists (tcons a i (tnil b)). now idtac. constructor. eexists. reflexivity. constructor; constructor. Qed.
imports: prop monoid positives comparisons