interpretation
"extensional equality (reducibility candidate)"
- 'napart C1 C2 = (rceq C1 C2).
+ 'Eq C1 C2 = (rceq C1 C2).
definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
interpretation
"extensional equality (context of reducibility candidates)"
- 'napart C1 C2 = (rceql C1 C2).
+ 'Eq C1 C2 = (rceql C1 C2).
theorem reflexive_rceq: reflexive … rceq.
/2/ qed.
(* HIDDEN BUG:
* Without the type specification, this statement has two interpretations
* but matita does not complain
- *)
-theorem mem_rceq_trans: â\88\80(M:T). â\88\80C1,C2. M â\88\88 C1 â\86\92 C1 â\89\88 C2 → M ∈ C2.
+ *)
+theorem mem_rceq_trans: â\88\80(M:T). â\88\80C1,C2. M â\88\88 C1 â\86\92 C1 â\89\85 C2 → M ∈ C2.
#M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
qed.
(* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
-theorem hd_repl: â\88\80C1,C2. C1 â\89\88 C2 â\86\92 â\88\80l1,l2. l1 â\89\88 l2 â\86\92 hd ? l1 C1 â\89\88 hd ? l2 C2.
+theorem hd_repl: â\88\80C1,C2. C1 â\89\85 C2 â\86\92 â\88\80l1,l2. l1 â\89\85 l2 â\86\92 hd ? l1 C1 â\89\85 hd ? l2 C2.
#C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
#hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
#hd2 #tl2 #_ #Q elim Q //
qed.
-theorem tl_repl: â\88\80l1,l2. l1 â\89\88 l2 â\86\92 tail ? l1 â\89\88 tail ? l2.
+theorem tl_repl: â\88\80l1,l2. l1 â\89\85 l2 â\86\92 tail ? l1 â\89\85 tail ? l2.
#l1 (elim l1) -l1 [ #l2 #Q >Q // ]
#hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
#hd2 #tl2 #_ #Q elim Q //
qed.
-theorem nth_repl: â\88\80C1,C2. C1 â\89\88 C2 â\86\92 â\88\80i,l1,l2. l1 â\89\88 l2 →
- nth i ? l1 C1 â\89\88 nth i ? l2 C2.
+theorem nth_repl: â\88\80C1,C2. C1 â\89\85 C2 â\86\92 â\88\80i,l1,l2. l1 â\89\85 l2 →
+ nth i ? l1 C1 â\89\85 nth i ? l2 C2.
#C1 #C2 #QC #i (elim i) /3/
qed.
definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
/2/ qed.
-theorem dep_repl: â\88\80B1,B2,C1,C2. B1 â\89\88 B2 â\86\92 C1 â\89\88 C2 →
- depRC B1 C1 â\89\88 depRC B2 C2.
+theorem dep_repl: â\88\80B1,B2,C1,C2. B1 â\89\85 B2 â\86\92 C1 â\89\85 C2 →
+ depRC B1 C1 â\89\85 depRC B2 C2.
#B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
[ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
qed.