case mk
α : Type u_1
β : Type ?u.28657
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode { val := val✝, property := property✝ } = encode ↑{ val := val✝, property := property✝ }
α : Type u_1
β : Type ?u.28657
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
⊢ encode a = encode ↑a
cases a
no goals
case mk
α : Type u_1
β : Type ?u.28657
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode { val := val✝, property := property✝ } = encode ↑{ val := val✝, property := property✝ }
rfl