proposition: Lemma decode_encode : ∏ (t : A ⨿ B) (p : code t), encode _ (decode _ p) = p.
proof: Proof. intro t. induction t. - cbn. intro p. induction p. apply idpath. - cbn. intro. apply fromempty. apply p. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA