More clean up

multris/channel/proto_model.v

@@ -145,7 +145,6 @@ Proof.
   intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by f_equiv.
 Qed.
 
-(* TODO: This is FALSE *)
 Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) :
   Proper ((≡) ==> impl) P →
   P proto_end → (∀ i x p, P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.