proposition: Lemma progress_ t τ : nil |-- t : τ → (exists t', reduce_congr t t') \/ value t.
proof: Proof. intros H; depind H; auto with term. destruct IHtypes1 as [[t' tt']|vt]. left; eauto with term. destruct IHtypes2 as [[u' uu']|vu]. left; eauto with term. depelim H; [depelim H|depelim vt..]. left. exists ([u]t0). eauto with term. destruct IHtypes1 as [[t' tt']|vt]; eauto with term. destruct IHtypes2 as [[u' uu']|vu]; eauto with term. destruct IHtypes as [[t' tt']|vt]; eauto with term. depelim vt; depelim H; eauto with term. depelim H. destruct IHtypes as [[t' tt']|vt]; eauto with term. depelim vt; depelim H; eauto with term. depelim H. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid