Skip to content
Snippets Groups Projects
Commit bc775a29 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Fixed typo in proto_model

parent 5e95b65a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
multris/channel/proto_model.v
+ 1
− 1
View file @ bc775a29
...@@ -180,7 +180,7 @@ Qed. ...@@ -180,7 +180,7 @@ Qed.
Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} : Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end. Inhabited (proto V PROPn PROP) := populate proto_end.
Lemma proto_message_equivI {Σ} `{V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 : Lemma proto_message_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2 proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p'). ⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
Proof. Proof.
......
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