proposition: Lemma form_prog_dec : (forall s t, reflect (s = t) (eqf s t)) * (forall a b, reflect (a = b) (eqp a b)).
proof: Proof. Proof with case => /=; try (constructor; discriminate). apply:form_prog_rect. - move... by constructor. - move => p... move => q. apply: (iffP eqP); congruence. - move => s IHs t IHt... move => s' t'. by apply: (iffP andP) => [[/IHs -> /IHt ->]|[/IHs ? /IHt ?]]. - move => s IHs t IHt... move => s' t'. by apply: (iffP andP) => [[/IHs -> /IHt ->]|[/IHs ? /IHt ?]]. - move => p... move => q. apply: (iffP eqP); congruence. - move => a IHa b IHb... move => a' b'. by apply: (iffP andP) => [[/IHa -> /IHb ->]|[/IHa ? /IHb ?]]. - move => a IHa s IHs... move => a' s'. by apply: (iffP andP) => [[/IHa -> /IHs ->]|[/IHa ? /IHs ?]]. - move => p IHp... move => q. apply: (iffP (IHp _)); congruence. - move => s IHs... move => t. apply: (iffP (IHs _)); congruence. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)