proposition: Lemma sa_env_refl : forall {n} (Γ : env O n), sa_env Γ Γ.
proof: Proof. depind Γ. depelim e. constructor. constructor; auto using sa_refl. Qed.
imports: Equations.Equations Equations.DepElimDec Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Program Arith