proposition: Lemma path_left_id : ∀ i j (x : Path (i,j)), path_compose Stop x = x.
proof: Proof. dependent destruction x; reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple