x : Char h : x = 'a' ⊢ x = 'a' x : Char h : x = 'A' ⊢ x = 'A' x : Char h : x = 'A' ⊢ x = 'A' x : String h : x = "a" ⊢ x = "a" x : Nat h : x = 65 ⊢ x = 65 x : Bool h : x = true ⊢ x = true x : Bool h : x = true ⊢ x = true x : Bool h : x = true ⊢ x = true x : Bool h : x = true ⊢ x = true x : Bool h : x = true ⊢ x = true x : Bool h : x = true ⊢ x = true x : UInt32 h : x = 65 ⊢ x = 65 x : Char h : x = 'A' ⊢ x = 'A' x : Bool h : x = false ⊢ x = false x : Bool h : x = true ⊢ x = true x : Prop h : ¬x ⊢ ¬x x : Prop h : x ⊢ x