proposition: Lemma prog_correct I l rel: (forall a, In (set.mem a) l) -> prog I l rel rel -> below_I I rel -> forall e f, In (e,f) rel -> sup lang e ≡ sup lang f.
proof: Proof. intros Hl Hrel Hvars e f Hef. rewrite <-2lang_sup, 2lang_lang'. intro w. revert e f Hef. induction w; simpl lang'; intros e f Hef. - apply Hrel in Hef as [_ Hef]. rewrite 2epsilon'_eq. destruct (Hef _ (Hl a)) as [-> _]. reflexivity. - destruct (fun H => In_dec H i I) as [Hi|Hi]. decide equality. etransitivity. apply lang'_weq. apply deriv'_eq. etransitivity. 2: apply lang'_weq; symmetry; apply deriv'_eq. apply IHw. apply Hrel. assumption. apply Hl. assumption. clear IHw. revert w. apply lang'_weq. rewrite 2deriv_sup. rewrite 2sup_b. reflexivity. intros f' Hf. eapply deriv_out. 2: eassumption. etransitivity. 2: apply Hvars. 2: apply Hef. apply leq_xsup. apply in_app_iff. now right. intros e' He. eapply deriv_out. 2: eassumption. etransitivity. 2: apply Hvars. 2: apply Hef. apply leq_xsup. apply in_app_iff. now left. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex