proposition: Theorem Step_deterministic Γ τ : deterministic (Step (Γ:=Γ) (τ:=τ)).
proof: Proof. repeat intro. induction H0. - inv H. + now f_equal; intuition. + eapply Value_cannot_start in H5; eauto; tauto. - inv H. + eapply Value_cannot_start in H3; eauto; tauto. + now f_equal; intuition. - inv H. + now f_equal; intuition. + inv H0. * eapply Value_cannot_start in H6; eauto; tauto. * eapply Value_cannot_start in H7; eauto; tauto. - inv H. + inv H3. * eapply Value_cannot_start in H1; eauto; tauto. * eapply Value_cannot_start in H7; eauto; tauto. + now f_equal; intuition. - inv H. + now f_equal; intuition. + inv H0. * eapply Value_cannot_start in H6; eauto; tauto. * eapply Value_cannot_start in H7; eauto; tauto. - inv H. + inv H3. * eapply Value_cannot_start in H1; eauto; tauto. * eapply Value_cannot_start in H7; eauto; tauto. + now f_equal; intuition. - inv H; auto. + now inv H3. + eapply Value_cannot_start in H7; eauto; tauto. - inv H. + now inv H0. + now f_equal; intuition. + now inv H0. - inv H. + eapply Value_cannot_start in H0; eauto; tauto. + eapply Value_cannot_start in H4; eauto; tauto. + now f_equal; intuition. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Category.Instance.Lambda.Sem Category.Instance.Lambda.Log Equations(Equations)