Buenas,
En el ejercicio 7 llegue a un punto en que tengo la siguiente meta e hipotesis:
Hpt : page_owned_by pt = Os (active_os s)
H7 : page_content pt = PT vm
______________________________________(1/3)
pt =
{|
page_content := PT vm;
page_owned_by := Os (active_os s)
|}
Es algo trivial, pero no encuentro la manera en coq de hacerlo.
Saludos.