proposition: Lemma lift_var_by_app : forall {b c} (p : scope_le b c) {a} (q : scope_le a b) t, lift_var_by p (lift_var_by q t) = lift_var_by (scope_le_app q p) t.
proof: Proof. Proof with autorewrite with lift_var_by map_var scope_le_app in *; auto. intros b c p; induction p; intros a q t... - rewrite IHp; auto. - generalize dependent p. generalize dependent t. depind q; intros... rewrite IHp... specialize (IHp _ q). rewrite (map_var_b (lift_var_by (scope_le_app q p)) (fun t => lift_var_by p (lift_var_by q t))); eauto. rewrite <- map_var_a; auto. Qed.
imports: Program Equations.Prop.DepElim Equations.Prop.Equations Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Arith