fact: Fixpoint dot_r m p (y: expr m p): forall n, expr n m -> expr n p := match y in syntax.expr _ _ m p return forall n, expr n m -> expr n p with | e_zer _ _ => fun n x => 0 | e_one _ => fun n x => x | e_pls y1 y2 => fun n x => if distribute then pls' (dot_r y1 x) (dot_r y2 x) else dot_l x (y1+y2) | e_dot y z => fun n x => dot_l (dot_r y x) z | y => fun n x => dot_l x y end%ast.
imports: kleene syntax powerfix