simplify; autobatch;
qed.
-notation > "'If' b 'Then' t 'Else' f"
-for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
+notation > "'If' b 'Then' t 'Else' f" non associative
+with precedence 90 for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
(* define the find function *)