fact: Fixpoint rule_of_rulechain (rc: rulechain) : rule := fun i => match rc with | [] => None | [r] => r i | r :: rules => match r i with | Some res => Some res | None => rule_of_rulechain rules i end end.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core