proposition: Lemma infer_sort_sound: forall (i : index) (ie: env) (s : sort), infer_sort i ie = Some s -> sorting ie i s.
proof: Proof. intros i ie. funelim (infer_sort i ie); intros s' Heqs; try (noconf Heqs || (rewrite Heq in *; noconf Heqs)). - now constructor. - now constructor. - specialize (Hind _ Heq). now constructor. - specialize (Hind _ Heq). now constructor. - pose proof (Hind _ Heq1). pose proof (Hind0 _ Heq2). subst s1. econstructor; eauto. Qed.
imports: Equations(Equations) Arith List ListSet Lia Program