proposition: Lemma enc_pair_inj {xy x'y'} : enc_pair xy = enc_pair x'y' -> xy = x'y'.
proof: Proof. move: xy x'y' => [x y] [x' y'] /=. rewrite pair_equal_spec. have : x + y <> x' + y' \/ x + y = x' + y' by lia. case; by nia. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun