fact: Definition expr_leq := powerfix 100 (fun leq tt n m (x: expr n m) p q (y: expr p q) => let leq {n m} x {p q} y := leq tt n m x p q y in match x,y with | e_zer _ _, _ | _, e_top _ _ | e_one _, e_one _ | e_one _, e_str _ => true | e_one _, e_itr y => leq x y | e_var a, e_var b => eqb a b | e_pls x x', _ => leq x y &&& leq x' y | _, e_cap y y' => leq x y &&& leq x y' | e_cap x x', _ => leq x y ||| leq x' y | _, e_pls y y' => leq x y ||| leq x y' | @e_dot _ _ _ _ u _ x x', @e_dot _ _ _ _ v _ y y' | @e_ldv _ _ _ u _ _ y x', @e_ldv _ _ _ v _ _ x y' | @e_rdv _ _ _ u _ _ y x', @e_rdv _ _ _ v _ _ x y' => eqb u v &&& leq x y &&& leq x' y' | e_one _, e_ldv x y | e_one _, e_rdv x y | e_neg y, e_neg x | e_itr x, e_itr y | e_itr x, e_str y | e_str x, e_str y | e_cnv x, e_cnv y => leq x y | _,_ => false end) (fun _ _ _ _ _ _ _ => false) tt.
imports: kleene syntax powerfix