proposition: Lemma lift_type_by_n : forall {n} (t : type n), lift_type_by scope_le_n t = t.
proof: Proof. intros; eapply lift_type_by_id; intros; autorewrite with lift_var_by; auto. Qed.
imports: Program Equations.Prop.DepElim Equations.Prop.Equations Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Arith