| inductive sublist : List α → List α → Prop | |
| | slnil : sublist [] [] | |
| | cons l₁ l₂ a : sublist l₁ l₂ → sublist l₁ (a :: l₂) | |
| | cons2 l₁ l₂ a : sublist l₁ l₂ → sublist (a :: l₁) (a :: l₂) | |
| #print sublist | |
| inductive Foo : List α → Type _ -- Make sure we don't need to use `_` or can use `u` | |
| | mk₁ : Foo [] | |
| | mk₂ : (a : α) → Foo as → Foo (a::as) | |
| inductive Bla : Foo as → Type _ | |
| | mk₁ : Bla Foo.mk₁ | |
| #print Foo | |
| #print Bla |