proposition: Lemma j_agree: forall E1 t T, j E1 t T -> forall E2 k, agree E1 E2 k -> length E1 <= k -> j E2 t T.
proof: Proof. induction 1; intros; eauto with j length agree lia. Qed.
imports: Coq.Program.Equality Dblib(DblibTactics DeBruijn Environments)