fact: Fixpoint fInT (f : rZ -> list triplet) (T : Trace) {struct T} : bool := match T with | emptyTrace => true | tripletTrace (Triplet b p q r) => match InDec _ tripletDec (Triplet b p q r) (f p) with | left _ => true | right _ => false end | seqTrace T1 T2 => match fInT f T1 with | true => fInT f T2 | false => false end | dilemmaTrace _ _ T1 T2 => match fInT f T1 with | true => fInT f T2 | false => false end end.
imports: Stalmarck(makeTriplet)