constant symbol Prop: TYPE;
injective symbol π: Prop → TYPE;
constant symbol Set: TYPE;
injective symbol τ:Set → TYPE;
constant symbol σℙ: Set → Set;
constant symbol = [T]: τ T → τ T → Prop;
notation = infix 10;

constant symbol ⊆ [T:Set]: τ (σℙ T) → τ (σℙ T) → Prop;
notation ⊆ infix 10;

constant symbol cset [T:Set]: (τ T → Prop) → τ (σℙ T);
notation cset quantifier;

constant symbol ℙ: Π [T:Set], τ (σℙ T) → τ (σℙ (σℙ T));

symbol isAll [T] (S: τ (σℙ T)): Prop ≔ (`cset u, u ⊆ S) = ℙ S;

symbol apply_erule [T]: τ T → τ T;
symbol check_erule [T] (e: τ T) : π (e = apply_erule e);

symbol prf : Π (T:Set) (S: τ (σℙ T)), π (isAll S);

rule apply_erule (`cset (x:τ (σℙ $T)), x ⊆ $S.[]) ↪ ℙ $S.[];

rule check_erule [(σℙ (σℙ $T))] (`cset x, x ⊆ $S.[]) ↪ prf $T $S;