proposition: Lemma well_founded_size A : well_founded (fun x y : seq A => size x < size y).
proof: Proof. by apply: (@Wf_nat.well_founded_lt_compat _ size) => ? ? /ltP. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)