proposition: Lemma two_level_rect (P: L → Type) (Pone: ∀ x, P (one x)) (Ptwo: ∀ x y, P (cons x (one y))) (Pmore: ∀ x y z, P z → (∀ y', P (cons y' z)) → P (cons x (cons y z))): ∀ l, P l.
proof: Proof. Proof with auto. cut (∀ l, P l * ∀ x, P (cons x l)). intros. apply X. destruct l... revert t. induction l... intros. split. apply IHl. intro. apply Pmore; intros; apply IHl. Qed.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation