proposition: Lemma codeK : pcancel encode decode.
proof: Proof. intro t. induction t. all: intuition. all: simpl. - rewrite IHt1. rewrite IHt2. reflexivity. - rewrite IHt1. rewrite IHt2. reflexivity. - rewrite IHt. reflexivity. - destruct n as [n npos]. cbn. destruct n. + discriminate. + cbn. rewrite -subnE subn0. repeat f_equal. apply eq_irrelevance. Defined.
imports: Coq(Utf8 Lia) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr realsum seq all_algebra fintype) Crypt(Prelude Axioms) extructures(ord fset fmap) Mon(SPropBase) Equations(Equations)