(* Destructions with pr_nat *************************************************)
lemma pr_after_nat_des (l) (l1):
- â\88\80f. @â\86\91â\9dªl1, fâ\9d« ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f →
- â\88\83â\88\83l2. @â\86\91â\9dªl1, f1â\9d« â\89\98 l2 & @â\86\91â\9dªl2, f2â\9d« ≘ l.
+ â\88\80f. @â\86\91â\9d¨l1, fâ\9d© ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f →
+ â\88\83â\88\83l2. @â\86\91â\9d¨l1, f1â\9d© â\89\98 l2 & @â\86\91â\9d¨l2, f2â\9d© ≘ l.
#l #l1 #f #H1 #f2 #f1 #Hf
elim (pr_after_pat_des … H1 … Hf) -f #i2 #H1 #H2
/2 width=3 by ex2_intro/
qed-.
lemma pr_after_des_nat (l) (l2) (l1):
- â\88\80f1,f2. @â\86\91â\9dªl1, f1â\9d« â\89\98 l2 â\86\92 @â\86\91â\9dªl2, f2â\9d« ≘ l →
- â\88\80f. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\86\91â\9dªl1, fâ\9d« ≘ l.
+ â\88\80f1,f2. @â\86\91â\9d¨l1, f1â\9d© â\89\98 l2 â\86\92 @â\86\91â\9d¨l2, f2â\9d© ≘ l →
+ â\88\80f. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\86\91â\9d¨l1, fâ\9d© ≘ l.
/2 width=6 by pr_after_des_pat/ qed-.
lemma pr_after_des_nat_sn (l1) (l):
- â\88\80f. @â\86\91â\9dªl1, fâ\9d« â\89\98 l â\86\92 â\88\80f1,l2. @â\86\91â\9dªl1, f1â\9d« ≘ l2 →
- â\88\80f2. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\86\91â\9dªl2, f2â\9d« ≘ l.
+ â\88\80f. @â\86\91â\9d¨l1, fâ\9d© â\89\98 l â\86\92 â\88\80f1,l2. @â\86\91â\9d¨l1, f1â\9d© ≘ l2 →
+ â\88\80f2. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\86\91â\9d¨l2, f2â\9d© ≘ l.
/2 width=6 by pr_after_des_pat_sn/ qed-.
lemma pr_after_des_nat_dx (l) (l2) (l1):
- â\88\80f,f2. @â\86\91â\9dªl1, fâ\9d« â\89\98 l â\86\92 @â\86\91â\9dªl2, f2â\9d« ≘ l →
- â\88\80f1. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\86\91â\9dªl1, f1â\9d« ≘ l2.
+ â\88\80f,f2. @â\86\91â\9d¨l1, fâ\9d© â\89\98 l â\86\92 @â\86\91â\9d¨l2, f2â\9d© ≘ l →
+ â\88\80f1. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\86\91â\9d¨l1, f1â\9d© ≘ l2.
/2 width=6 by pr_after_des_pat_dx/ qed-.