proposition: Lemma lang_atom n a: lang (g_atom n a) ≡ tatom n a.
proof: Proof. intros [b|]. 2: intros; compute; intuition discriminate. simpl. setoid_rewrite eval_var. split. intros H. now apply eval_atom in H as <-. intro E. injection E. clear E. intros <-. unfold atom. rewrite eval_inf. rewrite is_true_inf. intros i _. case_eq (set.mem a i); simpl; intros ->; reflexivity. Qed.
imports: lsyntax glang kat boolean atoms sups