proposition: Lemma ord_ind' (P: forall n, ord n -> Prop) (H0: forall n, P (S n) ord0) (HS: forall n i, P n i -> P (S n) (ordS i)): forall n i, P n i.
proof: Proof. induction n. intro i. elim (ord_0_empty i). destruct i as [[|i] Hi]. replace (Ord 0 Hi) with (@ord0 n) by now apply eq_ord. apply H0. replace (Ord (S i) Hi) with (ordS (@Ord n i Hi)) by now apply eq_ord. apply HS, IHn. Qed.
imports: List PeanoNat common comparisons