(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require Export arity_defs. (* NOTE: this preorder should be swapped *) Inductive csuba [g:G] : C -> C -> Prop := | csuba_sort: (n:?) (csuba g (CSort n) (CSort n)) | csuba_head: (c1,c2:?) (csuba g c1 c2) -> (k,u:?) (csuba g (CHead c1 k u) (CHead c2 k u)) | csuba_void: (c1,c2:?) (csuba g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?) (csuba g (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2)) | csuba_abst: (c1,c2:?) (csuba g c1 c2) -> (t:?; a:?) (arity g c1 t (asucc g a)) -> (u:?) (arity g c2 u a) -> (csuba g (CHead c1 (Bind Abst) t) (CHead c2 (Bind Abbr) u)). Hint csuba : ld := Constructors csuba. Section csuba_gen_base. (*************************************************) Lemma csuba_gen_abbr: (g:?; d1,c:?; u:?) (csuba g (CHead d1 (Bind Abbr) u) c) -> (EX d2 | c = (CHead d2 (Bind Abbr) u) & (csuba g d1 d2) ). Proof. Intros; InsertEq H '(CHead d1 (Bind Abbr) u); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 2. Qed. Lemma csuba_gen_void: (g:?; d1,c:?; u1:?) (csuba g (CHead d1 (Bind Void) u1) c) -> (EX b d2 u2 | c = (CHead d2 (Bind b) u2) & (csuba g d1 d2) ). Proof. Intros; InsertEq H '(CHead d1 (Bind Void) u1); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 2. Qed. Lemma csuba_gen_abst: (g:?; d1,c:?; u1:?) (csuba g (CHead d1 (Bind Abst) u1) c) -> (EX d2 | c = (CHead d2 (Bind Abst) u1) & (csuba g d1 d2) ) \/ (EX d2 u2 a | c = (CHead d2 (Bind Abbr) u2) & (csuba g d1 d2) & (arity g d1 u1 (asucc g a)) & (arity g d2 u2 a) ). Proof. Intros; InsertEq H '(CHead d1 (Bind Abst) u1); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 3. Qed. Lemma csuba_gen_flat: (g:?; d1,c:?; u1:?; f:?) (csuba g (CHead d1 (Flat f) u1) c) -> (EX d2 u2 | c = (CHead d2 (Flat f) u2) & (csuba g d1 d2) ). Proof. Intros; InsertEq H '(CHead d1 (Flat f) u1); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 2. Qed. Lemma csuba_gen_bind: (g:?; b1:?; e1,c2:?; v1:?) (csuba g (CHead e1 (Bind b1) v1) c2) -> (EX b2 e2 v2 | c2 = (CHead e2 (Bind b2) v2) & (csuba g e1 e2)). Proof. Intros; InsertEq H '(CHead e1 (Bind b1) v1); XElim H; Clear y c2; Intros; XInv; Subst; XDEAuto 2. Qed. Lemma csuba_gen_abst_rev: (g:?; d1,c:?; u:?) (csuba g c (CHead d1 (Bind Abst) u)) -> (EX d2 | c = (CHead d2 (Bind Abst) u) & (csuba g d2 d1) ) \/ (EX d2 u2 | c = (CHead d2 (Bind Void) u2) & (csuba g d2 d1) ). Proof. Intros; InsertEq H '(CHead d1 (Bind Abst) u); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 3. Qed. Lemma csuba_gen_void_rev: (g:?; d1,c:?; u:?) (csuba g c (CHead d1 (Bind Void) u)) -> (EX d2 | c = (CHead d2 (Bind Void) u) & (csuba g d2 d1) ). Proof. Intros; InsertEq H '(CHead d1 (Bind Void) u); XElim H; Clear y c; Intros; XInv; Subst; Try EqFalse; XDEAuto 2. Qed. Lemma csuba_gen_abbr_rev: (g:?; d1,c:?; u1:?) (csuba g c (CHead d1 (Bind Abbr) u1)) -> (OR (EX d2 | c = (CHead d2 (Bind Abbr) u1) & (csuba g d2 d1) ) | (EX d2 u2 a | c = (CHead d2 (Bind Abst) u2) & (csuba g d2 d1) & (arity g d2 u2 (asucc g a)) & (arity g d1 u1 a) ) | (EX d2 u2 | c = (CHead d2 (Bind Void) u2) & (csuba g d2 d1) )). Proof. Intros; InsertEq H '(CHead d1 (Bind Abbr) u1); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 3. Qed. Lemma csuba_gen_flat_rev: (g:?; d1,c:?; u1:?; f:?) (csuba g c (CHead d1 (Flat f) u1)) -> (EX d2 u2 | c = (CHead d2 (Flat f) u2) & (csuba g d2 d1) ). Proof. Intros; InsertEq H '(CHead d1 (Flat f) u1); XElim H; Clear y c; Intros; XInv; Subst; XDEAuto 2. Qed. Lemma csuba_gen_bind_rev: (g:?; b1:?; e1,c2:?; v1:?) (csuba g c2 (CHead e1 (Bind b1) v1)) -> (EX b2 e2 v2 | c2 = (CHead e2 (Bind b2) v2) & (csuba g e2 e1) ). Proof. Intros; InsertEq H '(CHead e1 (Bind b1) v1); XElim H; Clear y c2; Intros; XInv; Subst; XDEAuto 2. Qed. End csuba_gen_base. Tactic Definition CSubAGenBase := ( Match Context With | [ H: (csuba ? (CHead ? (Bind Abbr) ?) ?) |- ? ] -> XDecomPoseClear H '(csuba_gen_abbr ? ? ? ? H) | [ H: (csuba ? (CHead ? (Bind Void) ?) ?) |- ? ] -> XDecomPoseClear H '(csuba_gen_void ? ? ? ? H) | [ H: (csuba ? (CHead ? (Bind Abst) ?) ?) |- ? ] -> XDecomPoseClear H '(csuba_gen_abst ? ? ? ? H) | [ H: (csuba ? (CHead ? (Flat ?) ?) ?) |- ? ] -> XDecomPoseClear H '(csuba_gen_flat ? ? ? ? ? H) | [ H: (csuba ? (CHead ? (Bind ?) ?) ?) |- ? ] -> XDecomPoseClear H '(csuba_gen_bind ? ? ? ? ? H) | [ H: (csuba ? ? (CHead ? (Bind Abbr) ?)) |- ? ] -> XDecomPoseClear H '(csuba_gen_abbr_rev ? ? ? ? H) | [ H: (csuba ? ? (CHead ? (Bind Void) ?)) |- ? ] -> XDecomPoseClear H '(csuba_gen_void_rev ? ? ? ? H) | [ H: (csuba ? ? (CHead ? (Bind Abst) ?)) |- ? ] -> XDecomPoseClear H '(csuba_gen_abst_rev ? ? ? ? H) | [ H: (csuba ? ? (CHead ? (Flat ?) ?)) |- ? ] -> XDecomPoseClear H '(csuba_gen_flat_rev ? ? ? ? ? H) | [ H: (csuba ? ? (CHead ? (Bind ?) ?)) |- ? ] -> XDecomPoseClear H '(csuba_gen_bind_rev ? ? ? ? ? H) ). Section csuba_props. (****************************************************) Lemma csuba_refl: (g:?; c:?) (csuba g c c). Proof. XElim c; Intros; XAuto. Qed. Lemma csuba_clear_conf: (g:?; c1,c2:?) (csuba g c1 c2) -> (e1:?) (clear c1 e1) -> (EX e2 | (csuba g e1 e2) & (clear c2 e2)). Proof. Intros until 1; XElim H; Clear c1 c2; Intros; Try NewInduction k; ClearGenBase; Try (LApply (H0 e1); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0); XDEAuto 3. Qed. Lemma csuba_clear_trans: (g:?; c1,c2:?) (csuba g c2 c1) -> (e1:?) (clear c1 e1) -> (EX e2 | (csuba g e2 e1) & (clear c2 e2)). Proof. Intros until 1; XElim H; Clear c1 c2; Intros; Try NewInduction k; ClearGenBase; Try (LApply (H0 e1); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0); XDEAuto 3. Qed. End csuba_props. Hints Resolve csuba_refl : ld. Tactic Definition CSubAClear := ( Match Context With | [ H1: (csuba ?0 ?1 ?2); H2: (clear ?1 ?3) |- ? ] -> LApply (csuba_clear_conf ?0 ?1 ?2); [ Clear H1; Intros H1 | XAuto ]; LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ]; XDecompose H1 | [ H1: (csuba ?0 ?2 ?1); H2: (clear ?1 ?3) |- ? ] -> LApply (csuba_clear_trans ?0 ?1 ?2); [ Clear H1; Intros H1 | XAuto ]; LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ]; XDecompose H1 ). Section csuba_drop. (*****************************************************) Tactic Definition IH := ( Match Context With | [H0: (c1,d1:?; u1:?) (drop ?1 (0) c1 (CHead d1 ?2 u1)) -> (g:?; c2:?) (csuba g c1 c2) -> ?; H1: (drop (r (Bind ?) ?1) (0) ?0 (CHead ?3 ?2 ?4)); H2: (csuba ?5 ?0 ?7) |- ? ] -> LApply (H0 ?0 ?3 ?4); [ Clear H0 H1; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H2; Intros H0 | XAuto ]; XDecompose H0 | [H0: (d1:?; u1:?) (drop (S ?1) (0) ?0 (CHead d1 ?2 u1)) -> (g:?; c2:?) (csuba g ?0 c2) -> ?; H1: (drop (r (Flat ?) ?1) (0) ?0 (CHead ?3 ?2 ?4)); H2: (csuba ?5 ?0 ?7) |- ? ] -> LApply (H0 ?3 ?4); [ Clear H0 H1; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H2; Intros H0 | XAuto ]; XDecompose H0 | [H0: (c1,d1:?; u1:?) (drop ?1 (0) c1 (CHead d1 ?2 u1)) -> (g:?; c2:?) (csuba g c2 c1) -> ?; H1: (drop (r (Bind ?) ?1) (0) ?0 (CHead ?3 ?2 ?4)); H2: (csuba ?5 ?7 ?0) |- ? ] -> LApply (H0 ?0 ?3 ?4); [ Clear H0 H1; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H2; Intros H0 | XAuto ]; XDecompose H0 | [H0: (d1:?; u1:?) (drop (S ?1) (0) ?0 (CHead d1 ?2 u1)) -> (g:?; c2:?) (csuba g c2 ?0) -> ?; H1: (drop (r (Flat ?) ?1) (0) ?0 (CHead ?3 ?2 ?4)); H2: (csuba ?5 ?7 ?0) |- ? ] -> LApply (H0 ?3 ?4); [ Clear H0 H1; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H2; Intros H0 | XAuto ]; XDecompose H0 ). Lemma csuba_drop_abbr: (i:?; c1,d1:?; u:?) (drop i (0) c1 (CHead d1 (Bind Abbr) u)) -> (g:?; c2:?) (csuba g c1 c2) -> (EX d2 | (drop i (0) c2 (CHead d2 (Bind Abbr) u)) & (csuba g d1 d2) ). Proof. XElim i. (* case 1: i = 0 *) Intros; DropGenBase; Subst; CSubAGenBase; Subst; XDEAuto 2. (* case 2: i > 0 *) XElim c1; Intros. (* case 2.1: CSort *) DropGenBase; XInv; XInv. (* case 2.2: CHead *) DropGenBase; NewInduction k. (* case 2.2.1: Bind *) NewInduction b; CSubAGenBase; Subst; IH; XReplaceIn H1 n '(r (Bind Abbr) n); XDEAuto 3. (* case 2.2.2: Flat *) CSubAGenBase; Subst; IH; XDEAuto 3. Qed. Lemma csuba_drop_abst: (i:?; c1,d1:?; u1:?) (drop i (0) c1 (CHead d1 (Bind Abst) u1)) -> (g:?; c2:?) (csuba g c1 c2) -> (EX d2 | (drop i (0) c2 (CHead d2 (Bind Abst) u1)) & (csuba g d1 d2) ) \/ (EX d2 u2 a | (drop i (0) c2 (CHead d2 (Bind Abbr) u2)) & (csuba g d1 d2) & (arity g d1 u1 (asucc g a)) & (arity g d2 u2 a) ). Proof. XElim i. (* case 1: i = 0 *) Intros; DropGenBase; Subst; CSubAGenBase; Subst; XDEAuto 3. (* case 2: i > 0 *) XElim c1; Intros. (* case 2.1: CSort *) DropGenBase; XInv; XInv. (* case 2.2: CHead *) DropGenBase; NewInduction k. (* case 2.2.1: Bind *) NewInduction b; CSubAGenBase; Subst; IH; XReplaceIn H2 n '(r (Bind Abbr) n); XDEAuto 4. (* case 2.2.2: Flat *) CSubAGenBase; Subst; IH; XDEAuto 4. Qed. Lemma csuba_drop_abst_rev: (i:?; c1,d1:?; u:?) (drop i (0) c1 (CHead d1 (Bind Abst) u)) -> (g:?; c2:?) (csuba g c2 c1) -> (EX d2 | (drop i (0) c2 (CHead d2 (Bind Abst) u)) & (csuba g d2 d1) ) \/ (EX d2 u2 | (drop i (0) c2 (CHead d2 (Bind Void) u2)) & (csuba g d2 d1) ). Proof. XElim i. (* case 1: i = 0 *) Intros; DropGenBase; Subst; CSubAGenBase; Subst; XDEAuto 3. (* case 2: i > 0 *) XElim c1; Intros. (* case 2.1: CSort *) DropGenBase; XInv; XInv. (* case 2.2: CHead *) DropGenBase; NewInduction k. (* case 2.2.1: Bind *) NewInduction b; CSubAGenBase; Subst; IH; XDEAuto 4. (* case 2.2.2: Flat *) CSubAGenBase; Subst; IH; XDEAuto 4. Qed. Lemma csuba_drop_abbr_rev: (i:?; c1,d1:?; u1:?) (drop i (0) c1 (CHead d1 (Bind Abbr) u1)) -> (g:?; c2:?) (csuba g c2 c1) -> (OR (EX d2 | (drop i (0) c2 (CHead d2 (Bind Abbr) u1)) & (csuba g d2 d1) ) | (EX d2 u2 a | (drop i (0) c2 (CHead d2 (Bind Abst) u2)) & (csuba g d2 d1) & (arity g d2 u2 (asucc g a)) & (arity g d1 u1 a) ) | (EX d2 u2 | (drop i (0) c2 (CHead d2 (Bind Void) u2)) & (csuba g d2 d1) )). Proof. XElim i. (* case 1: i = 0 *) Intros; DropGenBase; Subst; CSubAGenBase; Subst; XDEAuto 3. (* case 2: i > 0 *) XElim c1; Intros. (* case 2.1: CSort *) DropGenBase; XInv; XInv. (* case 2.2: CHead *) DropGenBase; NewInduction k. (* case 2.2.1: Bind *) NewInduction b; CSubAGenBase; Subst; IH; XDEAuto 4. (* case 2.2.2: Flat *) CSubAGenBase; Subst; IH; XDEAuto 4. Qed. End csuba_drop. Tactic Definition CSubADrop := ( Match Context With | [ H0: (drop ?1 (0) ?2 (CHead ?3 (Bind Abbr) ?4)); H1: (csuba ?5 ?2 ?7) |- ? ] -> LApply (csuba_drop_abbr ?1 ?2 ?3 ?4); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 | [ H0: (drop ?1 (0) ?2 (CHead ?3 (Bind Abst) ?4)); H1: (csuba ?5 ?2 ?7) |- ? ] -> LApply (csuba_drop_abst ?1 ?2 ?3 ?4); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 | [ H0: (drop ?1 (0) ?2 (CHead ?3 (Bind Abbr) ?4)); H1: (csuba ?5 ?7 ?2) |- ? ] -> LApply (csuba_drop_abbr_rev ?1 ?2 ?3 ?4); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 | [ H0: (drop ?1 (0) ?2 (CHead ?3 (Bind Abst) ?4)); H1: (csuba ?5 ?7 ?2) |- ? ] -> LApply (csuba_drop_abst_rev ?1 ?2 ?3 ?4); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?5 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 ). Section csuba_getl. (*****************************************************) Lemma csuba_getl_abbr: (g:?; c1,d1:?; u:?; i:?) (getl i c1 (CHead d1 (Bind Abbr) u)) -> (c2:?) (csuba g c1 c2) -> (EX d2 | (getl i c2 (CHead d2 (Bind Abbr) u)) & (csuba g d1 d2) ). Proof. Intros until 1; GetLGenBase; NewInduction x; Try NewInduction k; ClearGenBase; Clear IHx. (* case 1: Bind *) XInv; Subst; CSubADrop; XDEAuto 3. (* case 2: Flat *) Impl H1 H0; UnIntro H1 c1. XElim i; Intros. (* case 2.1: i = 0 *) DropGenBase; Subst; Rename x into c. LApply (clear_flat c (CHead d1 (Bind Abbr) u)); [ Clear H1; Intros H1 | XAuto ]. XPoseClear H1 '(H1 f t); CSubAClear; CSubAGenBase; Subst; XDEAuto 3. (* case 2.2: i > 0 *) DropClear; CSubAClear; CSubAGenBase; Subst. LApply (H x2); [ Clear H H4; Intros H | XAuto ]. LApply (H x6); [ Clear H H5; Intros H | XAuto ]. XDecompose H; XDEAuto 3. Qed. Lemma csuba_getl_abst: (g:?; c1,d1:?; u1:?; i:?) (getl i c1 (CHead d1 (Bind Abst) u1)) -> (c2:?) (csuba g c1 c2) -> (EX d2 | (getl i c2 (CHead d2 (Bind Abst) u1)) & (csuba g d1 d2) ) \/ (EX d2 u2 a | (getl i c2 (CHead d2 (Bind Abbr) u2)) & (csuba g d1 d2) & (arity g d1 u1 (asucc g a)) & (arity g d2 u2 a) ). Proof. Intros until 1; GetLGenBase; NewInduction x; Try NewInduction k; ClearGenBase; Clear IHx. (* case 1: Bind *) XInv; Subst; CSubADrop; XDEAuto 4. (* case 2: Flat *) Impl H1 H0; UnIntro H1 c1. XElim i; Intros; Rename x into c. (* case 2.1: i = 0 *) DropGenBase; Subst. LApply (clear_flat c (CHead d1 (Bind Abst) u1)); [ Clear H1; Intros H1 | XAuto ]. XPoseClear H1 '(H1 f t); CSubAClear; CSubAGenBase; Subst; XDEAuto 4. (* case 2.2: i > 0 *) DropClear; CSubAClear; CSubAGenBase; Subst. LApply (H x2); [ Clear H H4; Intros H | XAuto ]. LApply (H x5); [ Clear H H5; Intros H | XAuto ]. XDecompose H; XDEAuto 4. Qed. Lemma csuba_getl_abst_rev: (g:?; c1,d1:?; u:?; i:?) (getl i c1 (CHead d1 (Bind Abst) u)) -> (c2:?) (csuba g c2 c1) -> (EX d2 | (getl i c2 (CHead d2 (Bind Abst) u)) & (csuba g d2 d1) ) \/ (EX d2 u2 | (getl i c2 (CHead d2 (Bind Void) u2)) & (csuba g d2 d1) ). Proof. Intros until 1; GetLGenBase; NewInduction x; Try NewInduction k; ClearGenBase; Clear IHx. (* case 1: Bind *) XInv; Subst; CSubADrop; XDEAuto 4. (* case 2: Flat *) Impl H1 H0; UnIntro H1 c1. XElim i; Intros; Rename x into c. (* case 2.1: i = 0 *) DropGenBase; Subst. LApply (clear_flat c (CHead d1 (Bind Abst) u)); [ Clear H1; Intros H1 | XAuto ]. XPoseClear H1 '(H1 f t); CSubAClear; CSubAGenBase; Subst; XDEAuto 4. (* case 2.2: i > 0 *) DropClear; CSubAClear; CSubAGenBase; Subst. LApply (H x2); [ Clear H H4; Intros H | XAuto ]. LApply (H x5); [ Clear H H5; Intros H | XAuto ]. XDecompose H; XDEAuto 4. Qed. Lemma csuba_getl_abbr_rev: (g:?; c1,d1:?; u1:?; i:?) (getl i c1 (CHead d1 (Bind Abbr) u1)) -> (c2:?) (csuba g c2 c1) -> (OR (EX d2 | (getl i c2 (CHead d2 (Bind Abbr) u1)) & (csuba g d2 d1) ) | (EX d2 u2 a | (getl i c2 (CHead d2 (Bind Abst) u2)) & (csuba g d2 d1) & (arity g d2 u2 (asucc g a)) & (arity g d1 u1 a) ) | (EX d2 u2 | (getl i c2 (CHead d2 (Bind Void) u2)) & (csuba g d2 d1) )). Proof. Intros until 1; GetLGenBase; NewInduction x; Try NewInduction k; ClearGenBase; Clear IHx. (* case 1: Bind *) XInv; Subst; CSubADrop; XDEAuto 4. (* case 2: Flat *) Impl H1 H0; UnIntro H1 c1. XElim i; Intros; Rename x into c. (* case 2.1: i = 0 *) DropGenBase; Subst. LApply (clear_flat c (CHead d1 (Bind Abbr) u1)); [ Clear H1; Intros H1 | XAuto ]. XPoseClear H1 '(H1 f t); CSubAClear; CSubAGenBase; Subst; XDEAuto 4. (* case 2.2: i > 0 *) DropClear; CSubAClear; CSubAGenBase; Subst. LApply (H x2); [ Clear H H4; Intros H | XAuto ]. LApply (H x5); [ Clear H H5; Intros H | XAuto ]. XDecompose H; XDEAuto 4. Qed. End csuba_getl. Tactic Definition CSubAGetL := ( Match Context With | [ H0: (getl ?1 ?2 (CHead ?3 (Bind Abbr) ?4)); H1: (csuba ?5 ?2 ?7) |- ? ] -> LApply (csuba_getl_abbr ?5 ?2 ?3 ?4 ?1); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 | [ H0: (getl ?1 ?2 (CHead ?3 (Bind Abst) ?4)); H1: (csuba ?5 ?2 ?7) |- ? ] -> LApply (csuba_getl_abst ?5 ?2 ?3 ?4 ?1); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 | [ H0: (getl ? ?0 (CHead ? (Bind Abbr) ?)); H1: (csuba ? ? ?0) |- ? ] -> XDecomPose '(csuba_getl_abbr_rev ? ? ? ? ? H0 ? H1); Clear H1 | [ H0: (getl ? ?0 (CHead ? (Bind Abst) ?)); H1: (csuba ? ? ?0) |- ? ] -> XDecomPose '(csuba_getl_abst_rev ? ? ? ? ? H0 ? H1); Clear H1 ).