proposition: Lemma eqDec_remove {X Y eqb} {H:eqbClass (X:=X) eqb} x x' (d:dec (x=x')) (a b : Y): (if d then a else b) = (if eqb x x' then a else b).
proof: Proof. apply dec_reflect_remove. eapply eqb_spec. Qed.
imports: Undecidability.L(L Tactics.LTactics LBool)