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