Update index.html

index.html

@@ -76,6 +76,9 @@ <h2>NF Consistency Proof</h2>
 I have claimed since 2010 to be in possession of a proof of the consistency of Quine's set theory New Foundations.<p>  
 
 <B>The formal verification of my proof of Con(NF) in Lean has been completed,</B> by Sky Wilshaw, a Part III student at Cambridge who is about to go on to her doctoral studies in Computer Science.<p>
+
+<A HREF="https://Randall-Holmes.github.io/Nfproof/maybedetangled2-for-arxiv.pdf">Here</A> is a newer version, reflecting collaboration of both authors, notably on improving the presentation of the Freedom of Action theorem.<p>
+
 <A HREF="https://Randall-Holmes.github.io/Nfproof/maybedetangled2.pdf">Here</A> is a version of the paper proof which is being edited to conform better with the approach that Sky took in the formalization.
 I have verified that the conclusions of the formal argument in Lean say the right thing:  it shows that there is a structure for the language of tangled type theory which satisfies all typed versions of statements in the finite axiomatization of NF due to Hailperin,
 which entails that it is in fact a model of tangled type theory, and so that New Foundations is consistent.  This version of the paper proof is still being edited to conform with the formalization,