(*** nexts_eq_repl *)
lemma pr_nexts_eq_repl (n):
- pr_eq_repl (λf1,f2. â\86\91*[n] f1 â\89¡ ↑*[n] f2).
+ pr_eq_repl (λf1,f2. â\86\91*[n] f1 â\89\90 ↑*[n] f2).
#n @(nat_ind_succ … n) -n
/3 width=5 by pr_eq_next/
qed.
(* Inversions with pr_eq ****************************************************)
lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2):
- â\86\91*[n1] ⫯f1 â\89¡ ↑*[n2] ⫯f2 →
- â\88§â\88§ n1 = n2 & f1 â\89¡ f2.
+ â\86\91*[n1] ⫯f1 â\89\90 ↑*[n2] ⫯f2 →
+ â\88§â\88§ n1 = n2 & f1 â\89\90 f2.
#f1 #f2
#n1 @(nat_ind_succ … n1) -n1 [| #n1 #IH ]
#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]