proposition: Lemma KP_5_iii n alpha beta: nf alpha -> nf beta -> const_pathS n alpha beta <-> KP_arrowS n alpha beta.
proof: Proof. intros H H0; split. - induction 1. + left; red. exists n; split; auto with arith. + right with y. * exists n; split. auto with arith. destruct H1; split; auto. * destruct H1 as [H02 H1]. apply IHclos_trans_1n;auto; subst y; now apply nf_canon. - induction 1. + destruct H1; destruct H1. apply Cor12_1 with x0;auto. * destruct H2; subst y; apply canonS_LT; auto. * left; split. -- intro; subst. inversion H2. now destruct H3. -- now destruct H2. + apply const_pathS_trans with y. * destruct H1; apply Cor12_1 with x0;auto. -- destruct H1 as [H1 H4]. destruct H1. ++ destruct H4; subst y; apply canonS_LT; auto. ++ destruct H4; subst; apply canonS_LT; auto. -- now destruct H1. -- destruct H1. destruct H3 as [H4 H5]; left; split; auto. * apply IHclos_trans_1n; auto. destruct H1 as [i [H2' [H2'' H2''']]]. subst; apply nf_canon; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)