doc: add wikidata attribute for Church-Rosser theorems (#626)

See [this
thread](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Wikipedia.20Day.202026.20Talk/with/582363210)
for context.

Author: chenson2018

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean

@@ -203,6 +203,7 @@ theorem para_confluence : Confluent (@Parallel Var) :=
   para_diamond.toConfluent
 
 /-- β-reduction is confluent. -/
+@[wikidata Q1308502]
 theorem confluence_beta : Confluent (@FullBeta Var) := by
   have eq : ReflTransGen (@Parallel Var) = ReflTransGen (@FullBeta Var) := by
     ext

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean

@@ -92,6 +92,7 @@ lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by
 
 open Commute in
 /-- βη-reduction is confluent. -/
+@[wikidata Q1308502]
 theorem confluent_beta_eta : Confluent (@FullBetaEta Var) := by
   apply join_confluent
   · exact confluence_beta

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean

@@ -34,6 +34,7 @@ open Relation
 variable [HasFresh Var] [DecidableEq Var]
 
 open FullEta in
+@[wikidata Q1308502]
 lemma stronglyConfluent_eta : StronglyConfluent (@FullEta Var) := by
   intro _ y z h₁ h₂
   suffices ∃ w, ReflGen FullEta y w ∧ ReflGen FullEta z w by grind