proposition: Lemma preserves_red1 Γ t τ : Γ |-- t : τ → forall u, t --> u → Γ |-- u : τ.
proof: Proof. intros H; induction H; intros t' redtt'; term; try find_empty; depelim redtt'. apply subst1 with A. now depelim H. apply H0. now depelim H. now depelim H. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid