fact: Fixpoint pls' n m (y: expr n m): expr n m -> expr n m := match y with | e_zer _ _ => fun x => x | e_top _ _ => fun y => top | e_pls y z => fun x => insert_pls (pls' y x) z | y => fun x => insert_pls x y end%ast.
imports: kleene syntax powerfix