proposition: Theorem eqb_kat_correct e f: eqb_kat e f = Some true -> e ≡ f.
proof: Proof. unfold eqb_kat. intro H. apply prog_loop in H as [rel [Hef Hrel]]. 2: intros _ _ []. 2: simpl vars; intros ? ? [E|[]]; injection E; intros <- <-; rewrite union_app, sup_app, 2sup_singleton; reflexivity. eapply prog_correct in Hrel. 2: intro; apply in_map, in_seq. 3: apply Hef; now left. rewrite 2sup_singleton in Hrel. assumption. intros ? ? ?. now apply Hrel. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex