. H,r:ind(z,x¯.T;a) >> Gagggggggby ind r over A ¯[EXT foobar]¯[EXT foobar] H,g: A> B , >> G by elim g on a new y H,g: A> B , >> a in {x:A | dom(g)(x)} H,g: A> B ,, y:B; y=g[a] in B >> G
>
H,g: A> B , >> a in {x:A | dom(g)(x)}
{
}
H,g: A> B ,, y:B; y=g[a] in B >> G
.
H,r:ind(z,x¯.T;a) >> G
a
g
ggggggby ind r over A 
¯[EXT foobar]¯[EXT foobar] H,g: A
>> G by elim g on a
new y
>> a in 
, y:B; y=g[a] in B >>
G