proposition: Lemma preserves_redpar Γ t τ : Γ |-- t : τ → forall u, reduce_congr t u → Γ |-- u : τ.
proof: Proof. intros H. induction H; intros t' rtt'; depelim rtt'; term; try find_empty. depelim H1. depelim H. eapply subst1; eauto. depelim H0; depelim H; term. depelim H0; depelim H; term. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid