proposition: Lemma length_lift_subst : forall G i, length (lift_subst G i) = length G.
proof: Proof. induction G. trivial. intro i; simpl. rewrite (IHG i); trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)