proposition: Lemma enc_inj {a b} : enc a = enc b -> a = b.
proof: Proof. rewrite /enc. move: (sym_eq_dec a a0) (sym_eq_dec a b0) (sym_eq_dec b a0) (sym_eq_dec b b0). move=> [] ? [] ? [] ? [] ? /=; try congruence. move: (a) (b) => [? [?|]] [? [?|]] /= [] /enc_pair_inj []; by congruence. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun