proposition: Lemma deqGSym : forall (G: CFGV), Deq (GSym G).
proof: Proof. intros. intros sa sb. destruct sa as [sa|sa|sa|sa]; destruct sb as [sb|sb|sb|sb]; try (right; introv Hc; inverts Hc; cpx; fail). - destruct (deqT G sa sb);[left; subst|right; introv HC; inverts HC]; cpx. - destruct (DeqVarSym G sa sb);[left; subst|right; introv HC; inverts HC]; cpx. - destruct (deqNT G sa sb);[left; subst|right; introv HC; inverts HC]; cpx. - destruct (deqPT G sa sb);[left; subst|right; introv HC; inverts HC]; cpx. Defined.
imports: GVariables