---

Step * 1 of Lemma sq_stable__alpha-aux


1. [opr] : Type
2. u : bound-term(opr)
3. v : bound-term(opr) List
4. ∀bt:bound-term(opr)
     ((bt ∈ [u / v]) ⇒ (∀b:term(opr). ∀vs,ws:varname() List.  SqStable(alpha-aux(opr;vs;ws;snd(bt);b))))
5. ∀f:opr. ∀b1:bound-term(opr) List. ∀f1:opr. ∀vs,ws:varname() List.
     SqStable(alpha-aux(opr;vs;ws;mkterm(f;v);mkterm(f1;b1)))
6. f : opr
7. u1 : bound-term(opr)
8. v1 : bound-term(opr) List
9. ∀f1:opr. ∀vs,ws:varname() List.  SqStable(alpha-aux(opr;vs;ws;mkterm(f;[u / v]);mkterm(f1;v1)))
10. f1 : opr
11. vs : varname() List
12. ws : varname() List
⊢ SqStable(let as,x = u 
           in let bs,y = u1 
              in (||as|| = ||bs|| ∈ ℤ) ∧ alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y))
BY
{ ((InstHyp [⌜u⌝] 4⋅ THENA Auto)
   THEN (DVar `u' THEN Reduce 0)
   THEN DVar `u1'
   THEN All Reduce
   THEN BLemma `sq_stable__and`
   THEN Try (BHyp -1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  u  :  bound-term(opr)
3.  v  :  bound-term(opr)  List
4.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  [u  /  v])
          {}\mRightarrow{}  (\mforall{}b:term(opr).  \mforall{}vs,ws:varname()  List.    SqStable(alpha-aux(opr;vs;ws;snd(bt);b))))
5.  \mforall{}f:opr.  \mforall{}b1:bound-term(opr)  List.  \mforall{}f1:opr.  \mforall{}vs,ws:varname()  List.
          SqStable(alpha-aux(opr;vs;ws;mkterm(f;v);mkterm(f1;b1)))
6.  f  :  opr
7.  u1  :  bound-term(opr)
8.  v1  :  bound-term(opr)  List
9.  \mforall{}f1:opr.  \mforall{}vs,ws:varname()  List.    SqStable(alpha-aux(opr;vs;ws;mkterm(f;[u  /  v]);mkterm(f1;v1)))
10.  f1  :  opr
11.  vs  :  varname()  List
12.  ws  :  varname()  List
\mvdash{}  SqStable(let  as,x  =  u 
                      in  let  bs,y  =  u1 
                            in  (||as||  =  ||bs||)  \mwedge{}  alpha-aux(opr;rev(as)  +  vs;rev(bs)  +  ws;x;y))


By

---

Latex:
((InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  (DVar  `u'  THEN  Reduce  0)
  THEN  DVar  `u1'
  THEN  All  Reduce
  THEN  BLemma  `sq\_stable\_\_and`
  THEN  Try  (BHyp  -1)
  THEN  Auto)

---

Home Index