fact: Fixpoint stripRzDec (S1 S2 : State) {struct S2} : State := match S2 with | nil => nil | (a, b) :: S'2 => match eqConstrStateDec S1 a b with | left _ => (a, b) :: stripRzDec S1 S'2 | right _ => stripRzDec S1 S'2 end end.
imports: Coq(List)