making the comment a bit more informative

theories/model.v

@@ -1150,25 +1150,28 @@ Qed.
 
 (* It seems safe to say that monotonicity is always easy *)
 (* to prove for all the programs that we expect to write. *)
-(* Thus, we will export ffix over monotone closure, but not ffix2. *)
-(* Exporting ffix has the advantage of eliding the always simple *)
+(* Thus, we will export Fix over monotone closure, but not Fix'. *)
+(* Exporting Fix has the advantage of eliding the always simple *)
 (* and syntax-directed proofs of monotonicity, which we just don't *)
 (* want to bother with. *)
 
-(* It isn't theoretically excluded that one may somehow concoct a *)
-(* non-monotone program using the exported syntax that will thus *)
-(* result in weird and incorrect specs, though I so far failed to do that. *)
-(* But if such a case arises it can be ruled out by switching to *)
-(* ffix2 and requiring an explicit proof of monotonicity. *)
-(* For all the examples we did so far, such a proof will be easily *)
-(* constructed, but will not be possible for the concocted example. *)
-
-(* Again, using ffix instead of ffix2 isn't some theoretically *)
-(* justified result, just an expedient design choice to avoid *)
-(* bothering with proofs that are always easy. *)
-(* Maybe the best of both worlds would be to instead design automation *)
-(* for proving monotonicity by simply traversing the recursive *)
-(* function and applying the command_mono lemmas *)
+(* This is in line with the existing proofs of soundness of HTT as a *)
+(* standalone theory, where you can show that all functions that can be *)
+(* produced using the syntax are monotone in the model. That proof *)
+(* relied on a significant subset of Coq, but still a subset. *)
+(* The paper is: *)
+(* Partiality, State and Dependent Types *)
+(* Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski *)
+(* International Conference on Typed Lambda Calculi and Applications (TLCA), pages 198-212, 2011. *)
+
+(* The model in that paper, and the one we use here, are quite different *)
+(* however, and we can't exclude concocting a *)
+(* non-monotone program using the syntax we export here, *)
+(* though we have so far failed to do that. *)
+(* But if such a case arises, we should switch to using Fix' *)
+(* and ask for explicit proofs of monotonicity. *)
+(* For all the examples we did so far, such a proof is easily *)
+(* constructed, along the lines of above (and maybe can even be automated). *)
 
 End MonotonicityExamples.