trying to prove false

Stream: lean4

[Arthur Paulino]

I was trying to trick the kernel with:

elab "intro_false" id:ident : tactic => do
  liftMetaTactic fun mvarId => do
    let mvarIdNew ← assert mvarId id.getId
      (mkApp2 (mkConst `Eq) (mkConst ``false) (mkConst ``true)) (mkConst `sorry)
    let (_, mvarIdNew) ← intro1P mvarIdNew
    return [mvarIdNew]

example : false := by
  intro_false h
  -- h : false = true
  -- ⊢ false = true
  assumption
  -- tactic 'assumption' failed
  -- h : false = true
  -- ⊢ false = true

But I don't understand why this doesn't work. Why is this so?

[Arthur Paulino]

exact h causes: incorrect number of universe levels Eq