proposition: Lemma ax_conv_test s t : prv ([t??^^]s <--> [t??]s).
proof: Proof. rule axEI. - rewrite -> ax_test. rewrite <- (ax_convEF t?? s) at 2. rewrite /EX. rewrite -> ax_test. do 3 Intro. by Apply. - rewrite -> (ax_convBB t?? [t??]s). apply: rNorm. rewrite /EX. do ! rewrite -> ax_test. rewrite -> dmI, axDNE. rule axAcase. do 2 Intro. by Apply. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)