Definition pairSequence {X} (A B : X) : Sequence X. Proof. exists 2. intros m. induction m as [m _]. induction m as [ | _ _]. - exact A. - exact B. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.