proposition: Lemma FL_trans_mut : (forall s t : form, t \in FL s -> FL t `<=` FL s) * (forall a (s t : form), t \in FL0 a s -> FL t `<=` FL0 a s `|` FL s).
proof: Proof. apply: form_prog_ind => /=. - fset_nocut. - fset_nocut. - move => s IHs t IHt u. rewrite !inE -orbA. case/or3P => [/eqP -> {t} //|/IHs|/IHt]; fset_nocut. - move => a IHa s IHs t /fsetUP [A|A]. + exact: IHa. + exact: sub_trans (IHs t A) _. - move => a s t. by rewrite inE => /eqP ->. - move => a IHa b IHb s t. rewrite !inE -orbA. case/or3P => [/eqP -> {t} //|A|A]. + move: (IHa _ _ A); fset_nocut. + move: (IHb _ _ A); fset_nocut. - move => a IHa b IHb s t. rewrite !inE -orbA. case/or3P => [/eqP -> {t} //|A|A]. + move: (IHa _ _ A); fset_nocut. + move: (IHb _ _ A); fset_nocut. - move => p IHp s t. case/fsetU1P => [ -> // |A]. move: (IHp _ _ A); fset_nocut. - move => u IHu s t /fsetU1P [-> // |A]. move: (IHu _ A); fset_nocut. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)