Skip to content
Snippets Groups Projects
Commit 015a5d52 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Simplify the proof of init_prod.

parent d2b01768
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/tests/init_prod.v
+ 1
− 1
View file @ 015a5d52
...@@ -26,7 +26,7 @@ Section rebor. ...@@ -26,7 +26,7 @@ Section rebor.
{ apply (uninit_product_subtype [] [] [1;1]%nat). } { apply (uninit_product_subtype [] [] [1;1]%nat). }
intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl. intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own. eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own.
eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own. eapply type_assign; try solve_typing. by apply write_own.
eapply type_delete; try solve_typing. eapply type_delete; try solve_typing.
eapply type_delete; try solve_typing. eapply type_delete; try solve_typing.
eapply (type_jump [_]); solve_typing. eapply (type_jump [_]); solve_typing.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment